0002021: Incorrect grammar for loop-behavior in document

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002021

Frama-C

Documentation > ACSL

public

2014-12-05 17:57

2016-01-26 08:52

Reporter

gaggarwal

Assigned To

patrick

Priority

normal

Severity

minor

Reproducibility

always

Status

closed

Resolution

fixed

Platform

OS Version

Product Version

Frama-C Neon-20140301

Target Version

Fixed in Version

Frama-C Magnesium

Summary

0002021: Incorrect grammar for loop-behavior in document

Description

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

Steps To Reproduce

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

Tags

No 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