View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0000758 | Frama-C | Plug-in > sparecode | public | 2011-03-21 10:41 | 2011-10-10 14:14 | ||||
Reporter | pherrmann | ||||||||
Assigned To | Anne | ||||||||
Priority | normal | Severity | major | Reproducibility | always | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Carbon-20110201 | ||||||||
Target Version | Fixed in Version | Frama-C Nitrogen-20111001 | |||||||
Summary | 0000758: Sparecode removes definitions which should be kept. | ||||||||
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. | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
Anne (reporter) 2011-03-21 13:54 |
Ok. I think that it is because the analysis doesn't go into global variables initialization, but I have to check... |
Anne (reporter) 2011-03-21 14:45 |
The problem was that the variable [tObjectRefInfo] is first declared, the used, then initialized later. It was assumed that a variable was declared and initialized before it was used... This will be fixed by my next commit, but please check that the obtained result is correct. |
pherrmann (reporter) 2011-03-21 15:05 |
I checked: the bug is corrected as of svn rev 12388. |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2011-03-21 10:41 | pherrmann | New Issue | |
2011-03-21 10:41 | pherrmann | Status | new => assigned |
2011-03-21 10:41 | pherrmann | Assigned To | => Anne |
2011-03-21 10:41 | pherrmann | File Added: bugspare.c | |
2011-03-21 10:43 | pherrmann | Product Version | Frama-C GIT, precise the release id => Frama-C Carbon-20110201 |
2011-03-21 10:43 | pherrmann | Summary | 12380 => Sparecode removes definitions which should be kept. |
2011-03-21 13:54 | Anne | Note Added: 0001613 | |
2011-03-21 13:54 | Anne | Status | assigned => acknowledged |
2011-03-21 14:45 | Anne | Note Added: 0001615 | |
2011-03-21 15:05 | pherrmann | Note Added: 0001616 | |
2011-03-21 15:05 | pherrmann | Status | acknowledged => resolved |
2011-05-16 17:28 | signoles | Resolution | open => fixed |
2011-10-10 14:13 | signoles | Fixed in Version | => Frama-C Nitrogen-20111001 |
2011-10-10 14:14 | signoles | Status | resolved => closed |