separately verified files show code-bug when linked together
ID0000615: This issue was created automatically from Mantis Issue 615. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000615 | Frama-C | Plug-in > jessie | public | 2010-10-22 | 2010-10-22 |
| Reporter | Jochen | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Boron-20100401 | Target Version | - | Fixed in Version | - |
Description :
The attached file contains the files "ftest3a.c" and "ftestMain.c. Each of them can be verified (by alt-ergo), except for "\valid(&b)" in ftestMain, cf. issue #614. Although the "assert res == 1" in ftestMain is verified, it does not hold, as can be seen by removing both "////"-comments, compiling, and running: "gcc ftest3a.c ftestMain.c && ./a.out" yields "main: res=0\n" on stdout. Note that the contracts of "f()" and "g()" are identical across both files, and that they don't omit neccessary or provide invalid preconditions (e.g. no "assigns \nothing"). Also, the "no-regions"-model is used in both files. The parameter "x" in "g()" is an alias to the global "b", and "f()" modifies "b". Both facts can be detected only by looking into ftestMain. Hence, by looking into ftest3a only, it cannot be detected that "g"s ensures clause is wrong; there is no other hint than nonexistent "assigns"-clauses.