Global invariants are not verified
ID0000373: This issue was created automatically from Mantis Issue 373. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000373 | Frama-C | Plug-in > jessie | public | 2010-01-14 | 2010-01-14 |
| Reporter | gmelquio | Assigned To | cmarche | Resolution | open |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C GIT, precise the release id | Target Version | - | Fixed in Version | - |
Description :
No proof obligations are generated for global invariants, which makes it easy to validate incorrect specifications.
/*@ global invariant toto: 0 == 1; / /@ ensures \result == 0; */ int main() { return 1; }
$ frama-c -jessie -jessie-atp=ergo b.c ... [jessie] Calling VCs generator. Running Alt-Ergo on proof obligations total : 1 valid : 1 (100%)