2021-03-05 07:24 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001563Frama-CPlug-in > obfuscatorpublic2013-11-21 13:452014-03-13 15:57
Reporterpatrick 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
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.
Attached Files

-Relationships
+Relationships

-Notes

~0004358

signoles (manager)

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

-Issue History
Date Modified Username Field Change
2013-11-21 13:45 patrick New Issue
2013-11-21 13:45 patrick Status new => assigned
2013-11-21 13:45 patrick Assigned To => signoles
2013-11-21 13:59 signoles Status assigned => confirmed
2013-11-21 13:59 signoles Target Version => Frama-C Neon-20140301
2013-12-02 17:37 signoles Note Added: 0004358
2013-12-02 17:37 signoles Status confirmed => resolved
2013-12-02 17:37 signoles Resolution open => fixed
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed
+Issue History