Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000250Frama-CPlug-in > obfuscatorpublic2009-09-18 15:592014-02-12 16:56
Reportervirgile 
Assigned Tomonate 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Beryllium-20090901 
Target VersionFixed in VersionFrama-C Beryllium-20090902 
Summary0000250: obfuscator loses link between logic and C variables
Descriptionon the code below,
//@ requires \valid(p);
void f(int * p);
int main(int * p)
{ f(p); }

executing frama-c -obfuscate t.c

returns
/*@ requires \valid(V1);
    */
extern void F1(int *G1 ) ;
int main(int *V3 )
{
  int V2 ;
  F1(V3);
  V2 = 0;
  return (V2);
}
i.e. the variable in the requires clause is not bound to the parameter of F1 anymore. It should be requires \valid(G1) instead.
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000410)
virgile (developer)
2009-09-21 11:46

This is only the case for specifications attached to prototypes.

- Issue History
Date Modified Username Field Change
2009-09-18 15:59 virgile New Issue
2009-09-18 15:59 virgile Status new => assigned
2009-09-18 15:59 virgile Assigned To => monate
2009-09-21 11:46 virgile Note Added: 0000410
2009-09-21 15:05 svn Checkin
2009-09-23 16:40 svn Checkin
2009-09-23 16:40 svn Status assigned => resolved
2009-09-23 16:40 svn Resolution open => fixed
2009-09-23 16:41 signoles Fixed in Version => Frama-C Beryllium 2
2009-09-23 20:22 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker