wrong proof obligation generated for loop initialization [under why-2.30]
ID0001007: This issue was created automatically from Mantis Issue 1007. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001007 | Frama-C | Kernel > ACSL implementation | public | 2011-11-03 | 2011-11-10 |
| Reporter | Jochen | Assigned To | virgile | Resolution | open |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Nitrogen-20111001 | Target Version | - | Fixed in Version | - |
Description :
Using Frama-C Nitrogen and Why 2.30, I ran the command "frama-c -cpp-command 'gcc -C -E -I.' -jessie -jessie-why-opt='-exp goal' -no-unicode -jessie-atp simplify ftest.c" on the attached program. The very first proof obligation formula, viz. ftest_ensures_default_po_1, has "iii" as a free variable, which is unusual.
The formula essentially says that a[0]==a[iii], which can neither be justified by the program code, nor by the loop invariant, nor by the function contract. I guess, the formula is intended to cover the loop initialization, but something like "FORALL (iii) (IMPLIES (EQ iii 0) ... )" is missing.