Frama-C Bug Tracking System - Frama-C
View Issue Details
0001450Frama-CKernelpublic2013-07-04 09:582013-09-26 12:27
patrick 
signoles 
normalminoralways
confirmedopen 
 
 
0001450: journalization of -print option
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
> 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; */
No tags attached.
Issue History
2013-07-04 09:58patrickNew Issue
2013-07-04 11:15signolesStatusnew => assigned
2013-07-04 11:15signolesAssigned To => signoles
2013-09-26 12:27signolesNote Added: 0004093
2013-09-26 12:27signolesStatusassigned => confirmed

Notes
(0004093)
signoles   
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.