Frama-C Bug Tracking System

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 
PlatformOSOS Version
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

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

- 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


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker