Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
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.
Attached Files

- Relationships

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


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker