2021-02-27 05:02 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0000862Frama-CKernel > ACSL implementationpublic2013-06-20 15:18
Assigned Tovirgile 
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0000862: ACSL parser + pretty-printer
Logic assertions of the form
(a) //@ assert x == y^z;

are parsed as (x==y)^y and are thus rejected by the type-checker. One must instead write the assertion above as follows

(b) //@ assert x == (y^z);

This may be understandable. The pretty-printer, however, after parsing the term (b), outputs the term (a), making the output of the pretty-printer a program that is syntactically invalid.

TagsNo tags attached.
Attached Files




signoles (manager)

Don't know exactly in which version this bug was fixed, but it does not appear anymore in Frama-C Fluorine.

The second form is correct and correctly outputs by the pretty-printer.

-Issue History
Date Modified Username Field Change
2011-06-10 10:19 ckunz New Issue
2011-06-10 10:19 ckunz Status new => assigned
2011-06-10 10:19 ckunz Assigned To => virgile
2013-06-20 15:18 signoles Note Added: 0003976
2013-06-20 15:18 signoles Status assigned => closed
2013-06-20 15:18 signoles Resolution open => fixed
2013-06-20 15:18 signoles Fixed in Version => Frama-C Fluorine-20130401
+Issue History