Frama-C Bug Tracking System - Frama-C
View Issue Details
0000862Frama-CKernel > ACSL implementationpublic2011-06-10 10:192013-06-20 15:18
Assigned Tovirgile 
PlatformOSOS Version
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

2013-06-20 15:18   
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
2011-06-10 10:19ckunzNew Issue
2011-06-10 10:19ckunzStatusnew => assigned
2011-06-10 10:19ckunzAssigned To => virgile
2013-06-20 15:18signolesNote Added: 0003976
2013-06-20 15:18signolesStatusassigned => closed
2013-06-20 15:18signolesResolutionopen => fixed
2013-06-20 15:18signolesFixed in Version => Frama-C Fluorine-20130401