GitLab

ID0001021: This issue was created automatically from Mantis Issue 1021. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0001021	Frama-C	Graphical User Interface	public	2011-11-18	2012-09-19

Reporter	patrick	Assigned To	yakobowski	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	have not tried
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Nitrogen-20111001	Target Version	-	Fixed in Version	Frama-C Oxygen-20120901

Description :

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.

Additional Information :

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