2021-01-15 18:51 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001450Frama-CKernelpublic2013-07-04 09:582013-09-26 12:27
Reporterpatrick 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityalways
StatusconfirmedResolutionopen 
Product Version 
Target VersionFixed in Version 
Summary0001450: journalization of -print option
DescriptionLoading 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;
 */

TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0004093

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.
+Notes

-Issue History
Date Modified Username Field Change
2013-07-04 09:58 patrick New Issue
2013-07-04 11:15 signoles Status new => assigned
2013-07-04 11:15 signoles Assigned To => signoles
2013-09-26 12:27 signoles Note Added: 0004093
2013-09-26 12:27 signoles Status assigned => confirmed
+Issue History