Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002021Frama-CDocumentation > ACSLpublic2014-12-05 17:572016-01-26 08:52
Reportergaggarwal 
Assigned Topatrick 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Neon-20140301 
Target VersionFixed in VersionFrama-C Magnesium 
Summary0002021: Incorrect grammar for loop-behavior in document
DescriptionGrammar for loop-behavior in Fig2.9 in acsl.pdf (http://frama-c.com/download/acsl.pdf [^]), page 36, has bug. loop-behavior has following grammar:

        loop-behavior := for id (, id)* : loop-clause*

which means that having atleast one loop clause is not necessary. But if I don't add any loop-clause frama-c throws warning: unexpected token ' ' in line XX
Steps To ReproduceFollowing example is correct as per the grammar of loop-behavior. But frama-c throws warning.

/*@ requires n>=0;
behavior fail :
   ensures \result == -1;
*/
int example(double t[], int n, double v ){
    int l=0, u= n-1;
    /*@ loop invariant 0 <=l && u <= n-1;
        for fail:
    */
    while(l <= u){
        l++;
    }
    return -1;
}

Note: this is contrived example
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006027)
patrick (developer)
2015-09-09 13:56

Accepted

- Issue History
Date Modified Username Field Change
2014-12-05 17:57 gaggarwal New Issue
2014-12-05 17:57 gaggarwal Status new => assigned
2014-12-05 17:57 gaggarwal Assigned To => signoles
2014-12-05 19:16 signoles Assigned To signoles => virgile
2015-09-07 15:27 signoles Assigned To virgile => patrick
2015-09-09 13:56 patrick Note Added: 0006027
2015-09-09 13:56 patrick Status assigned => resolved
2015-09-09 13:56 patrick Resolution open => fixed
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker