Description:
When using goto-instrument --k-induction with --step-case, the generated step case correctly adds an inductive hypothesis for assertions placed inside the loop body, but fails to do so for assertions placed after the loop. This makes it impossible to prove any post-loop property via k-induction, regardless of the value of k.
Case 1: Assertion inside the loop (works correctly)
int main() {
int x = 0;
int y = 0;
while (x < 10) {
x++;
y++;
__CPROVER_assert(y == x, "y == x"); // in-loop
}
}
Generated step case (k=1):
x := nondet
y := nondet
ASSUME y == x // inductive hypothesis correctly added
x := x + 1
y := y + 1
ASSERT y == x // check holds after one more step
ASSUME !(x < 10)
Result: VERIFICATION SUCCESSFUL at k=1.
Case 2: Assertion after the loop (broken)
int main() {
int x = 0;
int y = 0;
while (x < 10) {
x++;
y++;
}
__CPROVER_assert(y == x, "y == x"); // post-loop
}
Generated step case (k=1):
x := nondet
y := nondet
ASSUME !(x < 10) // assume loop has exited
ASSERT y == x // no inductive hypothesis 鈥?trivially unprovable
Result: VERIFICATION FAILED for all values of k.
Steps to reproduce Case 2:
goto-cc minimal.c -o minimal.gb
goto-instrument --k-induction 1 --base-case minimal.gb minimal.base.gb
goto-instrument --k-induction 1 --step-case minimal.gb minimal.step.gb
cbmc --no-signed-overflow-check minimal.base.gb # SUCCESSFUL
cbmc --no-signed-overflow-check minimal.step.gb # FAILED
Expected behaviour:
The step case for a post-loop assertion should include the assertion as an inductive hypothesis before the final loop iteration, analogous to how in-loop assertions are handled.
Observed behaviour:
x and y are independently havoc'd with no relationship assumed. The assertion is trivially unprovable and VERIFICATION FAILED is reported for all k.
Tested on: CBMC 6.8.0 (Ubuntu 24.04)
Description:
When using
goto-instrument --k-inductionwith--step-case, the generated step case correctly adds an inductive hypothesis for assertions placed inside the loop body, but fails to do so for assertions placed after the loop. This makes it impossible to prove any post-loop property via k-induction, regardless of the value of k.Case 1: Assertion inside the loop (works correctly)
Generated step case (k=1):
Result:
VERIFICATION SUCCESSFULat k=1.Case 2: Assertion after the loop (broken)
Generated step case (k=1):
Result:
VERIFICATION FAILEDfor all values of k.Steps to reproduce Case 2:
Expected behaviour:
The step case for a post-loop assertion should include the assertion as an inductive hypothesis before the final loop iteration, analogous to how in-loop assertions are handled.
Observed behaviour:
xandyare independently havoc'd with no relationship assumed. The assertion is trivially unprovable andVERIFICATION FAILEDis reported for all k.Tested on: CBMC 6.8.0 (Ubuntu 24.04)