Grammar omissions in 1.9
ID0002187: This issue was created automatically from Mantis Issue 2187. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002187 | Frama-C | Documentation > ACSL | public | 2015-11-23 | 2019-07-17 |
| Reporter | dcok@grammatech.com | Assigned To | patrick | Resolution | won't fix |
| Priority | normal | Severity | text | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | - |
Description :
Comments on the grammar in ACSL 1.9:
Corrections • There is no grammar for the \at, labelName, module, ::, open statement constructs • There is no grammar for the value of a logic array or union type (cf. Example 2.12). (The grammar of struct (record) values is in Fig. 2.16.) • In Fig. 2.11, including allocation-clause in a simple-clause-stmt is redundant, since it is already included in simple-clause. • The volatile declaration should end in a semicolon. (Fig. 2.26) • The grammar of a loop-behavior in Fig. 2.9 allows the for prefix, but no clauses. • The grammar allows a statement-contract and a behavior-body-stmt to have a completely empty set of clauses (Fig. 2.11), even with for prefixes.
Suggestions: • In Fig 2.12, the production for a C-external-declaration should allow global invariants, type invariants, model, module, and open declarations within one annotation, along with logic-def declarations, rather than in individual annotations as in Fig 2.23 and 2.24. • Volatile declarations should be allowed in annotations with other declarations. • Multiple assert specifications should be allowed in one annotation (Fig. 2.8)