Frama-C Bug Tracking System - Frama-C
View Issue Details
0000250Frama-CPlug-in > obfuscatorpublic2009-09-18 15:592014-02-12 16:56
virgile 
monate 
normalmajorhave not tried
closedfixed 
Frama-C Beryllium-20090901 
Frama-C Beryllium-20090902 
0000250: obfuscator loses link between logic and C variables
on 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.
No tags attached.
Issue History
2009-09-18 15:59virgileNew Issue
2009-09-18 15:59virgileStatusnew => assigned
2009-09-18 15:59virgileAssigned To => monate
2009-09-21 11:46virgileNote Added: 0000410
2009-09-21 15:05svnCheckin
2009-09-23 16:40svnCheckin
2009-09-23 16:40svnStatusassigned => resolved
2009-09-23 16:40svnResolutionopen => fixed
2009-09-23 16:41signolesFixed in Version => Frama-C Beryllium 2
2009-09-23 20:22signolesStatusresolved => closed

Notes
(0000410)
virgile   
2009-09-21 11:46   
This is only the case for specifications attached to prototypes.