failing unwinding assertion not properly supported

[prapicault]

PK "Property shown as failed even though the reason is a failing unwinding assertion. The corresponding loop could be highlighted. And a tool tip/hint to increase the unwinding bound should be shown."

[prapicault]

I'm not completely understanding the issue. Could you please provide an example that reproduces the issue?

[peterschrammel]

int x=0;
while(x<10) //c::main.0
{
assert(x<=5);
x++;
}
analyze with --unwind 2 or --unwindset c:main.0:2

[prapicault]

The failure entry in the trace does not include enough information to do the linking to the loop, and it is not clear how to distinguish between a problem with the unwinding limit and a real failure.

[peterschrammel]

The suffix number of the property name, e.g. "main.unwind.0" is the same as the one of the loop id, e.g. "main.0".

[prapicault]

So, is the cue the presence of "unwind" in the middle of the property name?

I'm moving this to an enhancement because in order to obtain the information required to do the proper presentation of the problem and provide linking to the loop section of the view; the view would have to read the counter example to extract the desired information, which it never had to do. So far reading the counter example was not necessary because it was sufficient to know the return code of CBMC to present the failure of a property in the view.

One way for CBMC to make it easier would be:
1 - provide a different exit code for such case so the view does not have to load every counter example
2 - optionally find a way to provide the problematic loop id in a more compact version

[peterschrammel]

I see. Then at least, during debugging the information can be displayed when the unwinding assertion has been reached.