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 - 2019 MantisBT Team
Powered by Mantis Bugtracker