Repository navigation
Is kInduction imprecise? #177
Description
Activity
Hi, in general, k-induction should not return
VERIFICATION FAILEDif it cannot find a counterexample reachable within the unwinding limit. We've usually experienced this behaviour when the program contained constructions not supported by 2LS (e.g. calls to various functions from the standard library) when 2LS over-approximated the effect of the construction which lead to an incorrect counterexample. Briefly looking at your example, I don't see any such construction but the program is rather difficult to read.The counterexample output when running in plain BMC mode with
2ls --inline --havoc --unwind 3 --trace bug.c.cis wrong. So, my suspicion is that there is a bug in the SSA translation.Hi,
I tried using cvise and 2ls to differentially reduce the example and got the following result:array_comp() { for (;;) return 0; } main() { if (array_comp()) __VERIFIER_error(); }
which gives
VERIFICATION SUCCESSFULfor--inlinebutVERIFICATION FAILEDfor--inline --k-induction,--inline --incremental-bmcand--inline --havoc --unwind 1
Seems pretty clear to me that the error should be unreachable, as array_comp always returns 0.
Hi,
I was wondering if the default kInduction analysis is meant to be precise, because running
2ls --inline --k-inductionon this safe program givesVERIFICATION FAILED(result should beSUCCESSFUL).Meanwhile the default analysis (i.e. just
2ls --inline) at least givesVERIFIFICATION INCONCLUSIVE.If I had to guess it's the combination of pointers and the Ternary Operator that is causing the problem, but I don't know for sure.
(array_comp(((long *)(array_Q_2)),(((unsigned char) (1U & (FV0))) ? (value_store(((long *)(FV26)),(unsigned int) ((FV1)),(unsigned int) ((BubbleSort_Q_0_Q_temp_Q_1)))) : ((long *)(array_Q_1))),ARRAY_SIZE)))Version: built from latest commit (c572aa1)
Thanks in advance,
Alex