Grammar omissions in 1.9
ID0002187: This issue was created automatically from Mantis Issue 2187. Further discussion may take place here.
|ID0002187||Frama-C||Documentation > ACSL||public||2015-11-23||2019-07-17|
|Reporterfirstname.lastname@example.org||Assigned To||patrick||Resolution||won't fix|
|Product Version||Frama-C Sodium||Target Version||-||Fixed in Version||-|
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)