Frama-C Bug Tracking System - Frama-C
View Issue Details
0001009Frama-CKernel > ACSL implementationpublic2011-11-04 13:222014-02-12 16:59
virgile 
virgile 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Oxygen-20120901 
0001009: code annotation placed above a local declaration are not correctly handled
with the attached file.i, frama-c -check file.i crashes. Apparently local x is not put in the appropriate block.
If you replace the assert with an ensures (arguably a function contract in this place does not mean anything), it is silently discarded.
No tags attached.
? file.i (61) 2011-11-04 13:22
https://bts.frama-c.com/file_download.php?file_id=290&type=bug
Issue History
2011-11-04 13:22virgileNew Issue
2011-11-04 13:22virgileStatusnew => assigned
2011-11-04 13:22virgileAssigned To => virgile
2011-11-04 13:22virgileFile Added: file.i
2011-11-09 09:12svnCheckin
2011-11-09 09:12svnStatusassigned => resolved
2011-11-09 09:12svnResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed
2014-02-12 16:59Note Added: 0004715
2014-02-12 16:59Statusclosed => resolved

Notes
(0004715)
   
2014-02-12 16:59   
Fix committed to stable/neon branch.