Frama-C Bug Tracking System - Frama-C
View Issue Details
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.
Relationships
Attached Files

Notes
(0000779)
signoles   
2010-04-19 16:14   
Fix in Why 2.24 (require Frama-C Boron-20100401).

Issue History
Date ModifiedUsernameFieldChange
2010-02-03 10:25signolesNew Issue
2010-02-03 10:25signolesStatusnew => assigned
2010-02-03 10:25signolesAssigned To => cmarche
2010-02-03 11:57cmarcheStatusassigned => resolved
2010-02-03 11:57cmarcheResolutionopen => fixed
2010-02-03 11:57cmarcheAdditional Information Updated
2010-04-19 16:13signolesStatusresolved => closed
2010-04-19 16:13signolesFixed in Version => Frama-C Boron
2010-04-19 16:14signolesNote Added: 0000779