2021-03-01 04:59 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000250Frama-CPlug-in > obfuscatorpublic2014-02-12 16:56
Reportervirgile 
Assigned Tomonate 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0000410

virgile (developer)

This is only the case for specifications attached to prototypes.
+Notes

-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
2009-09-23 16:40 svn
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
2013-12-19 01:13 Source_changeset_attached => framac master 9b289cba
2014-02-12 16:56 Source_changeset_attached => framac stable/neon 9b289cba
+Issue History