Frama-C Bug Tracking System - Frama-C
View Issue Details
0001563Frama-CPlug-in > obfuscatorpublic2013-11-21 13:452014-03-13 15:57
patrick 
signoles 
normalminorhave not tried
closedfixed 
 
Frama-C Neon-20140301Frama-C Neon-20140301 
0001563: Obfuscator for tags names in ACSL terms, properties, behaviors
Tags names in ACSL terms, properties, behaviors need to be obfucated.
> frama-c -obfuscate file.c /*@ behavior bhv: exits never: \false; complete behaviors bhv; */ int main(int f1) { int V1; V1 = 0; if (f1) goto end; V1 ++; /*@ assert property: V1 ? 1; */ ; end: ; return V1; }
No tags attached.
Issue History
2013-11-21 13:45patrickNew Issue
2013-11-21 13:45patrickStatusnew => assigned
2013-11-21 13:45patrickAssigned To => signoles
2013-11-21 13:59signolesStatusassigned => confirmed
2013-11-21 13:59signolesTarget Version => Frama-C Neon-20140301
2013-12-02 17:37signolesNote Added: 0004358
2013-12-02 17:37signolesStatusconfirmed => resolved
2013-12-02 17:37signolesResolutionopen => fixed
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

Notes
(0004358)
signoles   
2013-12-02 17:37   
Fixed. The obfuscator now handles property logic variables, behaviors and (identified) predicate. However, there are still some ACSL constructs which may contain unobfuscated names (not the one of the provided example though).