journalization of -print option
ID0001450: This issue was created automatically from Mantis Issue 1450. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001450 | Frama-C | Kernel | public | 2013-07-04 | 2013-09-26 |
| Reporter | patrick | Assigned To | signoles | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
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; */