Frama-C Bug Tracking System - Frama-C
View Issue Details
0001021Frama-CGraphical User Interfacepublic2011-11-18 13:542012-09-19 17:16
patrick 
yakobowski 
normalminorhave not tried
closedfixed 
Frama-C Nitrogen-20111001 
Frama-C Oxygen-20120901 
0001021: request for pretty printing only one property by lines
Sometimes, there is more than one property at a line. This is bad for the display of the property status. In GUI mode, the pretty printer should start the pretty printing of a statement at a new line when the statement has an annotation.
The following code: void f1 (void) { for (int i = 0; i < 10 ;) { //@ invariant i>=0; //@ assert i>=0; i++; } } is pretty printed as follow: void f1(void) { int i; i = 0; while (i < 10) { /*@ invariant i ? 0; */ ; /*@ assert i ? 0; */ ; i ++; } return; }
No tags attached.
Issue History
2011-11-18 13:54patrickNew Issue
2011-11-18 13:54patrickStatusnew => assigned
2011-11-18 13:54patrickAssigned To => monate
2011-11-18 13:54patrickAssigned Tomonate => yakobowski
2011-11-18 16:33yakobowskiNote Added: 0002478
2011-11-18 20:10yakobowskiNote Added: 0002480
2011-11-18 20:10yakobowskiStatusassigned => resolved
2011-11-18 20:10yakobowskiResolutionopen => fixed
2012-09-19 17:15signolesFixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16signolesStatusresolved => closed

Notes
(0002478)
yakobowski   
2011-11-18 16:33   
I won't do something special for the gui, so the change will impact all the Cil pretty-printers, and possibly all C code in general (even in absence of ACSL). Does someone object to that?
(0002480)
yakobowski   
2011-11-18 20:10   
Fixes in revision 16125. The code above is now printed as void f1(void) { int i; i = 0; while (i < 10) { /*@ invariant i ? 0; */ ; /*@ assert i ? 0; */ ; i ++; } return; } Some problems may remain with statement contracts. Feel free to reopen this bug if you find some.