2021-01-24 06:11 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000758Frama-CPlug-in > sparecodepublic2011-10-10 14:14
Reporterpherrmann 
Assigned ToAnne 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
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 Files
  • c file icon bugspare.c (962 bytes) 2011-03-21 10:41 -
    struct tClassInfo;
    struct tObjectRefInfo;
    struct ARedef;
    typedef int (*tFunPtr)(struct ARedef*, long);
    
    struct tClassInfo {
       tFunPtr *methodArray ;
       int isNotInit ;
    };
    
    struct tObjectRefInfo {
      struct tClassInfo *info ;
    };
    
    struct ARedef {
      struct tObjectRefInfo *refInfo ;
      long a_ARedef ;
    };
    
    
    int set_a_ARedef(struct ARedef *this , long _bcvar1 ) 
    {
      this->a_ARedef = _bcvar1;
      return 0;
    }
    
    tFunPtr methodArray_ARedef[2] = 
      {(tFunPtr)(& set_a_ARedef),
       (tFunPtr)(& set_a_ARedef)};
    
    struct tClassInfo classInfo_ARedef  = {(tFunPtr *)(& methodArray_ARedef), 1};
    struct tObjectRefInfo refInfo_ARedef ;
    
    int main(void) 
    {
      struct ARedef aredef ;
      int res;
    
      tFunPtr tmpMethodPtr;
    
      aredef.refInfo = & refInfo_ARedef;
    
      tmpMethodPtr = *(aredef.refInfo->info->methodArray[1]);
      res = (*tmpMethodPtr)((struct ARedef *)&aredef,
    			(long )1);
      return res;
    }
    
    struct tObjectRefInfo refInfo_ARedef  = { (struct tClassInfo *)(& classInfo_ARedef) };
    
    
    
    c file icon bugspare.c (962 bytes) 2011-03-21 10:41 +

-Relationships
+Relationships

-Notes

~0001613

Anne (reporter)

Ok. I think that it is because the analysis doesn't go into global variables initialization, but I have to check...

~0001615

Anne (reporter)

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)

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

-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: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
+Issue History