Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000529Frama-CPlug-in > sparecodepublic2010-07-06 12:372010-12-17 19:36
Reporterpascal 
Assigned ToAnne 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000529: slicing produces uncompilable program when formal used as a local variable
DescriptionAlu:day_2 pascal$ cat s.c
main(int x, int y, int z){
  int A, B;
  A = x;
  y = A;
  B = y;
  return B;
}

Alu:day_2 pascal$ frama-c -sparecode-analysis s.c
...
/* Generated by Frama-C */
int main(int x )
{
  int A ;
  int B ;
  A = x;
  y = A;
  B = y;
  return (B);
}

The generated program misses a declaration for y.
TagsNo tags attached.
Relationships
Attached Files

There are no notes attached to this issue.

Issue History
Date ModifiedUsernameFieldChange
2010-07-06 12:37pascalNew Issue
2010-07-06 12:37pascalStatusnew => assigned
2010-07-06 12:37pascalAssigned To => Anne
2010-07-06 16:26signolesCategoryPlug-in > slicing => Plug-in > sparecode
2010-07-06 16:53AnneStatusassigned => resolved
2010-07-06 16:53AnneResolutionopen => fixed
2010-12-10 15:45signolesFixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36signolesStatusresolved => closed