Incorrectness when early exiting a block
ID0001740: This issue was created automatically from Mantis Issue 1740. Further discussion may take place here.
|Plug-in > E-ACSL
|Fixed in Version
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.