Frama-C Bug Tracking System
Main | My View | View Issues | Change Log | Roadmap | Repositories
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000391Frama-CPlug-in > jessiepublic2010-02-03 10:252010-04-19 16:14
Reportersignoles 
Assigned Tocmarche 
PrioritynormalSeveritytweakReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in VersionFrama-C Boron-20100401 
Summary0000391: Why keywords as ACSL identifiers
DescriptionThe generated why file contains a syntax error (a keyword is used where an identifier is expected).
Steps To Reproduce=== t.c ===
/*@ lemma rec: \true; */
===========

$ frama-c -jessie t.c
File "why/t.why", line 94, characters 5-8:
Syntax error
Additional Information
Fixed in Why CVS
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0000779)
signoles (manager)
2010-04-19 16:14

 Fix in Why 2.24 (require Frama-C Boron-20100401).

- Issue History
Date Modified Username Field Change
2010-02-03 10:25 signoles New Issue
2010-02-03 10:25 signoles Status new => assigned
2010-02-03 10:25 signoles Assigned To => cmarche
2010-02-03 11:57 cmarche Status assigned => resolved
2010-02-03 11:57 cmarche Resolution open => fixed
2010-02-03 11:57 cmarche Additional Information Updated
2010-04-19 16:13 signoles Status resolved => closed
2010-04-19 16:13 signoles Fixed in Version => Frama-C Boron
2010-04-19 16:14 signoles Note Added: 0000779

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker