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
Assigned Tovirgile 
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
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 - 2020 MantisBT Team
Powered by Mantis Bugtracker