Open gsingh93 opened 2 years ago
I'm actually not sure if --unwind 9
is working, this doesn't seem right (there are no VCCs):
Runtime Symex: 0.0015976s
size of program expression: 78 steps
simple slicing removed 0 assignments
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 2.2844e-05s
VERIFICATION SUCCESSFUL
The CBMC unwinder and the goto-instrument unwinder are actually different bits of code that work differently. The CBMC unwinder is done as part of symbolic execution and counts the number of back-edges taken. The goto-instrument unwinder works by manipulating the goto-program by copying the loop body.
The CBMC symex does constant folding which is why you are seeing no VCCs with --unwind 9
, if you allow the back edge to be taken 9 times, on the 9th one i = 8
so the branch condition fails and so the unwinding assertion is not generated as it can never be reached.
This is, sort of, an off-by-one error but it is more that the numbers are measuring different things. This is, from a user point of view, not really ideal.
CBMC version: 5.42.0 (cbmc-5.42.0-2-g038a53b50) Operating system: Debian Exact command line resulting in the issue:
cbmc --unwind 8 --unwinding-assertions test.c --function foo
What behaviour did you expect: No assertions should fail What happened instead: Assertions fail, unless I use--unwind 9
instead of--unwind 8
I have the following code in
test.c
:The loop should iterate 8 times. If I perform the unwinding with
goto-instrument
, everything works as expected:In the output I have no verification errors and I see
[foo.1] line 3 assertion: SUCCESS
. If I use--unwind 7
instead it fails as expected.But when I use CBMC directly, this fails:
I see
[foo.unwind.0] line 3 unwinding assertion loop 0: FAILURE
. However, using--unwind 9
works.Is there an off-by-one issue here, or am I misunderstanding something?