2021-02-24 18:30 CET
  

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 
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
+Relationships

-Notes

~0001057

virgile (developer)

2010-08-18 11:11

 fixed in svn
+Notes

-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-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
+Issue History