| 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 | |
| Platform | | OS | | OS Version | |
| 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 | |
|
Relationships 
Relationships