Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #545

Incorrect grammar for loop-behavior in document

ID0002021: This issue was created automatically from Mantis Issue 2021. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002021 Frama-C Documentation > ACSL public 2014-12-05 2016-01-26
Reporter gaggarwal Assigned To patrick Resolution fixed
Priority normal Severity minor Reproducibility always
Platform - OS - OS Version -
Product Version Frama-C Neon-20140301 Target Version - Fixed in Version Frama-C Magnesium

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

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking