Incorrectness when early exiting a block
ID0001740: This issue was created automatically from Mantis Issue 1740. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001740 | Frama-C | Plug-in > E-ACSL | public | 2014-04-07 | 2017-05-31 |
| Reporter | signoles | Assigned To | signoles | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | Frama-C 15-Phosphorus |
Description :
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.