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