Incorrectness when early exiting a block
ID0001740: This issue was created automatically from Mantis Issue 1740. Further discussion may take place here.
|ID0001740||Frama-C||Plug-in > E-ACSL||public||2014-04-07||2017-05-31|
|Product Version||-||Target Version||-||Fixed in Version||Frama-C 15-Phosphorus|
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.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information