obfuscator loses link between logic and C variables
ID0000250: This issue was created automatically from Mantis Issue 250. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0000250 | Frama-C | Plug-in > obfuscator | public | 2009-09-18 | 2014-02-12 |
| Reporter | virgile | Assigned To | monate | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Beryllium-20090901 | Target Version | - | Fixed in Version | Frama-C Beryllium-20090902 |
Description :
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.