Skip to content

request for pretty printing only one property by lines

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information