Sparecode removes definitions which should be kept.
ID0000758: This issue was created automatically from Mantis Issue 758. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000758 | Frama-C | Plug-in > sparecode | public | 2011-03-21 | 2011-10-10 |
| Reporter | pherrmann | Assigned To | Anne | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Carbon-20110201 | Target Version | - | Fixed in Version | Frama-C Nitrogen-20111001 |
Description :
Sparecode removes definitions which should be kept.
See attached file bugspare.c. Perform sparecode analysis, then value analysis on resulting code.
frama-c-gui -sparecode-analysis /opt/bugspare.c -then-on "default without sparecode" -val
First analysis is correct: the function pointer gets a correct value.
After spare code analysis, some definitions are incorrectly removed (in particular, classInfo_ARedef), and the function pointer takes an uninitialized value.
Attachments
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information