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