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.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information