Frama-C Bug Tracking System - Frama-C
View Issue Details
0001740Frama-CPlug-in > E-ACSLpublic2014-04-07 13:572017-05-31 19:05
signoles 
signoles 
normalmajoralways
closedfixed 
 
Frama-C 15-Phosphorus 
0001740: Incorrectness when early exiting a block
Local variables of a block are de-allocated at the end of the block. However, they are not de-allocated when exiting a block earlier (e.g. by a goto or a break). That may lead to incorrectness as in the attached example. $ frama-c -e-acsl a.i -then-on e-acsl -print -ocode b.i $ ./gcc.sh b.i compiling b.i executing b.i Assertion failed at line 13 in function main. The failing predicate is: !\valid(p). No error should be detected.
No tags attached.
? a.i (156) 2014-04-07 13:57
https://bts.frama-c.com/file_download.php?file_id=723&type=bug
Issue History
2014-04-07 13:57signolesNew Issue
2014-04-07 13:57signolesStatusnew => assigned
2014-04-07 13:57signolesAssigned To => signoles
2014-04-07 13:57signolesFile Added: a.i
2014-04-07 13:57signolesStatusassigned => confirmed
2017-03-02 15:18kvorobyovStatusconfirmed => resolved
2017-03-02 15:18kvorobyovResolutionopen => fixed
2017-05-31 19:04signolesFixed in Version => Frama-C 15-Phosphorus
2017-05-31 19:05signolesStatusresolved => closed

There are no notes attached to this issue.