Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
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.
Attached Filesc file icon bugspare.c [^] (962 bytes) 2011-03-21 10:41 [Show Content]

- Relationships

-  Notes
(0001613)
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...
(0001615)
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.
(0001616)
pherrmann (reporter)
2011-03-21 15:05

I checked: the bug is corrected as of svn rev 12388.

- Issue History
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:08 Anne Note Added: 0001614
2011-03-21 14:41 Anne Note Deleted: 0001614
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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker