Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000758Frama-CPlug-in > sparecodepublic2011-03-21 10:412011-10-10 14:14
Reporterpherrmann 
Assigned ToAnne 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000758: Sparecode removes definitions which should be kept.
DescriptionSparecode 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.


TagsNo tags attached.
Relationships
Attached Filesc bugspare.c (962) 2011-03-21 10:41
https://bts.frama-c.com/file_download.php?file_id=184&type=bug

Notes
(0001613)
Anne   
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...
(0001615)
Anne   
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.
(0001616)
pherrmann   
2011-03-21 15:05   
I checked: the bug is corrected as of svn rev 12388.

Issue History
Date ModifiedUsernameFieldChange
2011-03-21 10:41pherrmannNew Issue
2011-03-21 10:41pherrmannStatusnew => assigned
2011-03-21 10:41pherrmannAssigned To => Anne
2011-03-21 10:41pherrmannFile Added: bugspare.c
2011-03-21 10:43pherrmannProduct VersionFrama-C GIT, precise the release id => Frama-C Carbon-20110201
2011-03-21 10:43pherrmannSummary12380 => Sparecode removes definitions which should be kept.
2011-03-21 13:54AnneNote Added: 0001613
2011-03-21 13:54AnneStatusassigned => acknowledged
2011-03-21 14:45AnneNote Added: 0001615
2011-03-21 15:05pherrmannNote Added: 0001616
2011-03-21 15:05pherrmannStatusacknowledged => resolved
2011-05-16 17:28signolesResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed