Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001009Frama-CKernel > ACSL implementationpublic2011-11-04 13:222014-02-12 16:59
Reportervirgile 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001009: code annotation placed above a local declaration are not correctly handled
Descriptionwith the attached file.i, frama-c -check file.i crashes. Apparently local x is not put in the appropriate block.
Additional InformationIf you replace the assert with an ensures (arguably a function contract in this place does not mean anything), it is silently discarded.
TagsNo tags attached.
Attached Files? file icon file.i [^] (61 bytes) 2011-11-04 13:22 [Show Content]

- Relationships

-  Notes
(0004715)

2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-11-04 13:22 virgile New Issue
2011-11-04 13:22 virgile Status new => assigned
2011-11-04 13:22 virgile Assigned To => virgile
2011-11-04 13:22 virgile File Added: file.i
2011-11-09 09:12 svn Checkin
2011-11-09 09:12 svn Status assigned => resolved
2011-11-09 09:12 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2014-02-12 16:59 Note Added: 0004715
2014-02-12 16:59 Status closed => resolved


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker