CBMC Toy Example

Question

I'm new to CBMC and experimenting with it. In this link here, there is a toy example for checking the function binsearch with CBMC. I decided to run the following command that they provided, just changing up the number of times the loop was unwound:

cbmc binsearch.c --function binsearch --unwind 4 --bounds-check --unwinding-assertions

It returned the following:

** Results:
[binsearch.unwind.0] unwinding assertion loop 0: FAILURE
prog.c function binsearch
[binsearch.array_bounds.1] line 7 array `a' lower bound in a[(signed long int)middle]: SUCCESS
[binsearch.array_bounds.2] line 7 array `a' upper bound in a[(signed long int)middle]: SUCCESS
[binsearch.array_bounds.3] line 9 array `a' lower bound in a[(signed long int)middle]: SUCCESS
[binsearch.array_bounds.4] line 9 array `a' upper bound in a[(signed long int)middle]: SUCCESS

Is the fact that the unwinding assertion failed because there weren't enough iterations a bad thing? From my point-of-view, it seems like the example is bug-free because the code didn't access portions of memory that it's not supposed to, but I'm not sure based on that one unwinding assertions failure. Anyone have any ideas about the safety? Does that failure matter?

Answer 1

Based on the --unwinding-assertion property, which checks the following:

Checks whether --unwind is large enough to cover all program paths. If the argument is too small, CBMC will detect that not enough unwinding is done reports that an unwinding assertion has failed.

I'd say that it is alerts to the possibility that there aren't enough loop iterations to make sure that the function won't access the array outside of the bounds. This means that while the function didn't violate any properties with 4, we need to check all paths before we can say that it is safe for certain.