contract completely ignored if preceeded by initial comment
ID0001819: This issue was created automatically from Mantis Issue 1819. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001819 | Frama-Clang | Plug-in > clang | public | 2014-06-27 | 2014-09-26 |
| Reporter | Jochen | Assigned To | virgile | Resolution | fixed |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | xubuntu-cfe13.10 (64 bit) | OS Version | - |
| Product Version | Frama-C Neon-20140301 | Target Version | - | Fixed in Version | Frama-C GIT, precise the release id |
Description :
Running "frama-c -wp -wp-rte Fault2.cpp -wp-out Fault2_64" on the attached program produces the attached file "_Z3fooi_assert.ergo", corresponding to the "assert" in line 8, but no .ergo file for the (non-trivial) "ensures" in line 5. The proof obligation in file "_Z3fooi_assert.ergo" shows that the requires from line 4 has been ignored, too.
In the gui, no contract at all is shown in the (left-hand side) normalized-code window.
The problem disappears if (1) the file is renamed to "Fault2.c", or (2) the comment is moved after the "requires" clause (, or removed completely).