Report inability of verification

[bitcalc]

I want to use SMACK to achieve high confidence by formally verifying certain properties. This requires SMACK to report assertions that it fails to verify after runs. For example, I have code

0: int buf[10];
1: int i = 0, x;
2: while(complicated_confition) {
3: …
4: i++;
5: }
6: assert(i + 12 < 10);
7: x = buf[i + 12];

When I run SMACK with --unroll=2, it silently completes without any warning. SMACK cannot determine that the while loop exits in this run and finishes as if the verification succeeded. It makes us lose confidence in verified code when it completes.

A much-needed feature is to give a user feedback on which assertions that SMACK decides to give up, which could come in different flavors.

1. Ideally, SMACK should report which assertions it doesn't verify after a run.
2. If the above is too difficult, then SMACK should report the loops that it cannot determinate their exits so that we know assertions inside and/or after the loops are not verified.

This information warns a user that SMACK doesn't finish all verification tasks, although it doesn't help solve them. Without this information, a user doesn't know if a normal completion means a successful verification or trivial non-verification.