View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0001563 | Frama-C | Plug-in > obfuscator | public | 2013-11-21 13:45 | 2014-03-13 15:57 | ||||
Reporter | patrick | ||||||||
Assigned To | signoles | ||||||||
Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | |||||||||
Target Version | Frama-C Neon-20140301 | Fixed in Version | Frama-C Neon-20140301 | ||||||
Summary | 0001563: Obfuscator for tags names in ACSL terms, properties, behaviors | ||||||||
Description | Tags 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; } | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
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). |
![]() |
|||
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 |