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.