0001450: journalization of -print option - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

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

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