Frama-C Bug Tracking System - Frama-C
View Issue Details
0002276Frama-CGraphical User Interfacepublic2017-02-03 09:282017-11-27 10:25
Max P. 
maroneze 
normaltweakalways
acknowledgedreopened 
Frama-C 14-Silicon 
 
0002276: Duplicates are created on the tab "Messages"
New messages append to old messages on the tab "Messages" if an analysis are rerun with new options.
1. Run Value analysis. 2. Change any option. 3. Run Value analysis.
No tags attached.
Issue History
2017-02-03 09:28Max P.New Issue
2017-02-03 09:28Max P.Statusnew => assigned
2017-02-03 09:28Max P.Assigned To => maroneze
2017-02-03 13:43maronezeNote Added: 0006352
2017-02-03 13:43maronezeStatusassigned => closed
2017-02-03 13:43maronezeResolutionopen => won't fix
2017-02-03 16:51Max P.Note Added: 0006354
2017-02-03 16:51Max P.Statusclosed => feedback
2017-02-03 16:51Max P.Resolutionwon't fix => reopened
2017-02-03 17:12Max P.Note Edited: 0006354View Revisions
2017-02-06 08:34Max P.Note Edited: 0006354View Revisions
2017-11-27 10:25maronezeNote Added: 0006474
2017-11-27 10:25maronezeStatusfeedback => acknowledged

Notes
(0006352)
maroneze   
2017-02-03 13:43   
This is intentional, although it might be considered counter-intuitive. Running subsequent analyses in the GUI is equivalent to using command-line option `-then`, which exhibits the same behavior as you described. This behavior makes more sense when running different plug-ins (e.g. derived Value plug-ins such as Nonterm), each of them emitting different messages. It also makes sense for other plug-ins such as WP, which are modular, and therefore likely to be executed several times in sequence. For a whole-program analysis such as Value, this makes little sense. The recommended approach when using Value is to parse and parameterize it using the command-line, and then use the GUI mainly to inspect results (falling back to the command-line for further parameterization).
(0006354)
Max P.   
2017-02-03 16:51   
(edited on: 2017-02-06 08:34)
Maybe you should add a button "Clear messages"? Even better would be to check whether there is such a record and do not add a duplicate. It is not always possible to achieve the desired at a time. See https://bts.frama-c.com/view.php?id=2277
(0006474)
maroneze   
2017-11-27 10:25   
The logging mechanism in the GUI is due to be revamped in a future release and the new behavior will likely prevent this situation from happening.