Frama-C Bug Tracking System - Frama-C
View Issue Details
0002021Frama-CDocumentation > ACSLpublic2014-12-05 17:572016-01-26 08:52
gaggarwal 
patrick 
normalminoralways
closedfixed 
Frama-C Neon-20140301 
Frama-C Magnesium 
0002021: Incorrect grammar for loop-behavior in document
Grammar 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
Following 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
No tags attached.
Issue History
2014-12-05 17:57gaggarwalNew Issue
2014-12-05 17:57gaggarwalStatusnew => assigned
2014-12-05 17:57gaggarwalAssigned To => signoles
2014-12-05 19:16signolesAssigned Tosignoles => virgile
2015-09-07 15:27signolesAssigned Tovirgile => patrick
2015-09-09 13:56patrickNote Added: 0006027
2015-09-09 13:56patrickStatusassigned => resolved
2015-09-09 13:56patrickResolutionopen => fixed
2016-01-26 08:51signolesFixed in Version => Frama-C Magnesium
2016-01-26 08:52signolesStatusresolved => closed
2016-06-21 14:11signolesCategoryDocumentation => Documentation > ACSL

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