|View Issue Details|
|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|
|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.|
|Ok. I think that it is because the analysis doesn't go into global variables initialization, but I have to check...|
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.
|I checked: the bug is corrected as of svn rev 12388.|
|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|