Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000079Frama-CKernel > ACSL implementationpublic2009-05-11 16:232010-02-05 09:44
Reporterboris 
Assigned Tovirgile 
PrioritynormalSeverityfeatureReproducibilityalways
StatusassignedResolutionopen 
PlatformOSOS Version
Product VersionFrama-C Lithium-20081201 
Target VersionFixed in Version 
Summary0000079: Better support of //@ style
DescriptionAnnotation consisting of several //@ lines should be supported. Eg, the following code produces a syntax error, whereas the /*@ ... */ style works: //@ loop invariant a[0] == 1; //@ loop invariant 1 <= i; for(i=1; i<10; i++)
TagsNo tags attached.
Attached Files

- Relationships
related to 0000365closedcmarche Jessie tutorial binary_search examples fail with Why 2.23 - loop variant must be added 

-  Notes
(0000052)
monate (reporter)
2009-05-11 19:59

This is conformant with ACSL grammar for loop annotations. Only one special comment is attached to the following loop. /*@ loop invariant a[0] == 1; */ /*@ loop invariant 1 <= i; */ for(i=1; i<10; i++) is also incorrect.
(0000614)
dwheeler (reporter)
2010-01-04 17:41

I agree with this proposal. If this isn't done, at *least* provide much clearer error reports. Currently, given two lines of the form: //@ ... //@ ... The system error messages point to lines FAR further down, making debugging the REAL problem very difficult (due to the terribly misleading reference).

- Issue History
Date Modified Username Field Change
2009-05-11 16:23 boris New Issue
2009-05-11 19:59 monate Note Added: 0000052
2009-05-15 11:09 monate Status new => assigned
2009-05-15 11:09 monate Assigned To => virgile
2009-06-17 13:38 signoles Category plug-in > jessie => kernel
2010-01-04 17:41 dwheeler Note Added: 0000614
2010-01-05 08:41 signoles Relationship added related to 0000365
2010-02-05 09:44 signoles Category Kernel => Kernel > ACSL implementation


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker