Frama-C Bug Tracking System - Frama-C
View Issue Details
IDProjectCategoryView StatusDate SubmittedLast Update
0000862Frama-CKernel > ACSL implementationpublic2011-06-10 10:192013-06-20 15:18
Reporterckunz 
Assigned Tovirgile 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0000862: ACSL parser + pretty-printer
Description
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.
Relationships
Attached Files

Notes
(0003976)
signoles   
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
Date ModifiedUsernameFieldChange
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