Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0001563Frama-CPlug-in > obfuscatorpublic2013-11-21 13:452014-03-13 15:57
Reporterpatrick 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFrama-C Neon-20140301Fixed in VersionFrama-C Neon-20140301 
Summary0001563: Obfuscator for tags names in ACSL terms, properties, behaviors
DescriptionTags names in ACSL terms, properties, behaviors need to be obfucated.
Additional Information> 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;
}

TagsNo tags attached.
Relationships
Attached Files

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).

Issue History
Date ModifiedUsernameFieldChange
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