View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|
0001450 | Frama-C | Kernel | public | 2013-07-04 09:58 | 2013-09-26 12:27 | ||||||||
Reporter | patrick | ||||||||||||
Assigned To | signoles | ||||||||||||
Priority | normal | Severity | minor | Reproducibility | always | ||||||||
Status | confirmed | Resolution | open | ||||||||||
Product Version | |||||||||||||
Target Version | Fixed in Version | ||||||||||||
Summary | 0001450: journalization of -print option | ||||||||||||
Description | Loading a script file issued previously with -journal-enable option should perform the same job as previously done. That is not the case with -print option: Once the -print option is journalized, executing that journal performs two print! > frama-c -print file.c -journal-enable > frama-c -load-script frama_c_journal.ml | ||||||||||||
Additional Information | > cat file.c //@ lemma l : 1 == 1; > frama-c -print file.c -journal-enable [kernel] preprocessing with "gcc -C -E -I. file.c" /* Generated by Frama-C */ /*@ lemma l: 1 ? 1; */ [kernel] writing journal in file `frama_c_journal.ml'. > frama-c -load-script frama_c_journal.ml [kernel] preprocessing with "gcc -C -E -I. file.c" /* Generated by Frama-C */ /*@ lemma l: 1 ? 1; */ /* Generated by Frama-C */ /*@ lemma l: 1 ? 1; */ | ||||||||||||
Tags | No tags attached. | ||||||||||||
Attached Files |
|
![]() |
|
signoles (manager) 2013-09-26 12:27 |
Not so easy to fix. Would require either: - to memoize the AST printer (that is not so easy with the current implementation actually); or - not to journalize the -print option, but I'm unsure that is something we want. |