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)