Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000538Frama-CKernelpublic2010-07-09 14:092010-12-17 19:36
Reporterboris 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Boron-20100401 
Target VersionFixed in VersionFrama-C Carbon-20101201-beta1 
Summary0000538: Frama-C should produce more specific error messages when parsing annotations
DescriptionIf an annotation contains a syntax error, Frama-C should be more specific about the kind of error.

For example, given a source file that contains this line

//@ loop invariant \forall integer i; aLength-1 >= i > high ==> a[i] > val);

a more helpful report may be:

foo.c, line 24: ')' unexpected
//@ loop invariant \forall integer i; aLength-1 >= i > high ==> a[i] > val);
                                                                             ^ here
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0001057)
virgile (developer)
2010-08-18 11:11

fixed in svn

- Issue History
Date Modified Username Field Change
2010-07-09 14:09 boris New Issue
2010-07-12 02:35 pascal Summary Frama-C should produce more specific error messages on annotations => Frama-C should produce more specific error messages when parsing annotations
2010-07-16 15:13 monate Status new => acknowledged
2010-08-15 20:13 pascal Relationship added has duplicate 0000553
2010-08-17 16:58 virgile Status acknowledged => assigned
2010-08-17 16:58 virgile Assigned To => virgile
2010-08-17 16:58 virgile Status assigned => confirmed
2010-08-18 11:11 virgile Note Added: 0001057
2010-08-18 11:11 virgile Status confirmed => resolved
2010-08-18 11:11 virgile Resolution open => fixed
2010-12-10 15:45 signoles Fixed in Version => Frama-C Carbon-20101201-beta1
2010-12-17 19:36 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker