invalid statement contract ("assigns") verified with CVC4 under strange circumstances
ID0002110: This issue was created automatically from Mantis Issue 2110. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002110 | Frama-Clang | Plug-in > wp | public | 2015-04-30 | 2015-09-07 |
| Reporter | Jochen | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Sodium-20150201 | OS | - | OS Version | xubuntu14.04 |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp-prover cvc4 -wp 473.c" on the attached file (referred to as version "(0)" in the modification discussion below) results in verifying all proof obligations, including the statement contract in line 27, which is obviously false, since "myRead" also assigns "fd->pos" (line 13) and definitely changes it (line 15). I can't see a contradiction from which line 27 could be proven.
CVC4 still proves all obligations if one of the following changes is made: (+1) myRead's "assigns" clauses in line 13 and 14 are joined into a single one, viz. "assigns fd->pos,*a;" (+2) all "requires" clauses in line 10-12 and 20-22 are commented-in simultaneously
CVC4 fails to prove the statement contract in line 27 if one of the following changes is made: (-1) myRead's "assigns" clauses in line 13 and 14 are swapped, (-2) myRead's "assigns" clauses in line 13 and 14 are joined into a single "assigns a,fd->pos;" (-3) the "ensures" clauses in line 15 is deleted (-4) the "ensures" clauses in line 23 (i.e. the whole contract) is deleted (-5) the type of "a" is changed from "struct A" to "int*" in line 17 and 25
From (+1) vs. (-2), as well as from (0) vs. (-1), it seems that the order of the memory location specifiers in myRead's "assigns" clause does matter. In (0) vs. (-4), the "ensures" clause of "myMain" apparently influences its body code.