Probably, CBMC have a hard time unwinding a loop

[DennisYurichev]

CBMC 5.10.
https://yurichev.com/news/20210421_boyer_moore/
I unwound the loop manually, that helped.
(Or maybe I should try other CBMC options...)
Am I right CBMC can't unwind a loop where iterator is modified inside a body?

[tautschnig]

Would you please share the exact command line you're using, and perhaps also the exact code? I'm assuming this is about your code variant unsigned search_cat_BM_v1 (char *s, unsigned len). If that's the case, then I'd guess that the increment to i is input-dependent (the value of skip can either be 1 or 3). Hence, the value of i cannot be constant-propagated, and CBMC will have to keep unrolling. If these guesses are correct, then one way of handling such an example is running CBMC with --unwind <some known bound> --unwinding-assertions to keep CBMC from unwinding until it runs out of resources while still ensuring soundness.

[DennisYurichev]

https://yurichev.com/news/20210421_boyer_moore/files/for_GCC/BM_cat_v1.c
https://yurichev.com/news/20210421_boyer_moore/files/for_GCC/BM_cat_v2.c
I can't wait till this finish: cbmc --trace --function check -DLEN=10 -DCBMC BM_cat_v1.c
As you suggest, I can prove it using: cbmc --trace --function check -DLEN=10 -DCBMC --unwind 100 --unwinding-assertions BM_cat_v1.c
Fine, but how I can be sure 100 is enough?

[danielsn]

The --unwinding-assertions will fail if the bound is not large enough

[tautschnig]

Resolving as guidance has been provided (and the same is documented).