syntax error in contract causes rest to be tacitly ignored
ID0001821: This issue was created automatically from Mantis Issue 1821. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001821 | Frama-Clang | Plug-in > clang | public | 2014-06-27 | 2015-04-16 |
| 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 | - |
Description :
Running "frama-c-gui -wp -wp-rte Fault2.cpp" on the attached program causes a message "Fault2.cpp:4:2: expecting function spec" on stderr (that's ok), but doesn't prevent the gui to appear (that's at least different to the behavior on a renamed version "Fault2.c"). More important, no error or warning message is visible in the gui (I checked the tabs "Information", "Messages", "Console", "Properties", "WP Goals"), and the contract rest after the error is tacitly ignored.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information