Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000373Frama-CPlug-in > jessiepublic2010-01-14 10:392010-01-14 10:39
Reportergmelquio 
Assigned Tocmarche 
PrioritynormalSeveritymajorReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0000373: Global invariants are not verified
DescriptionNo 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%)
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2010-01-14 10:39 gmelquio New Issue
2010-01-14 10:39 gmelquio Status new => assigned
2010-01-14 10:39 gmelquio Assigned To => cmarche


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker