Frama-C Bug Tracking System - Frama-C
View Issue Details
0002187Frama-CDocumentation > ACSLpublic2015-11-23 02:212019-07-17 10:59
dcok@grammatech.com 
patrick 
normaltextN/A
closedwon't fix 
Frama-C Sodium 
 
0002187: Grammar omissions in 1.9
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)
No tags attached.
Issue History
2015-11-23 02:21dcok@grammatech.comNew Issue
2015-11-23 02:21dcok@grammatech.comStatusnew => assigned
2015-11-23 02:21dcok@grammatech.comAssigned To => signoles
2015-11-23 04:20signolesAssigned Tosignoles => maroneze
2016-06-21 14:11signolesCategoryDocumentation => Documentation > ACSL
2016-06-21 14:26signolesAssigned Tomaroneze => patrick
2016-06-22 08:28patrickNote Added: 0006211
2016-06-22 08:38patrickNote Added: 0006212
2016-06-22 08:46patrickNote Edited: 0006212bug_revision_view_page.php?bugnote_id=6212#r267
2016-06-22 08:56patrickNote Edited: 0006211bug_revision_view_page.php?bugnote_id=6211#r269
2016-06-22 08:56patrickNote Edited: 0006211bug_revision_view_page.php?bugnote_id=6211#r270
2016-06-22 11:25patrickNote Added: 0006213
2016-07-22 08:05patrickNote Added: 0006238
2016-07-22 08:08patrickNote Edited: 0006238bug_revision_view_page.php?bugnote_id=6238#r279
2016-07-22 08:21patrickNote Added: 0006239
2016-07-22 08:25patrickNote Added: 0006240
2016-07-22 08:37patrickNote Edited: 0006239bug_revision_view_page.php?bugnote_id=6239#r281
2019-07-17 10:59patrickNote Added: 0006822
2019-07-17 10:59patrickStatusassigned => closed
2019-07-17 10:59patrickResolutionopen => won't fix

Notes
(0006211)
patrick   
2016-06-22 08:28   
(edited on: 2016-06-22 08:56)
The following points were fixed into ACSL 1.11:
• 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.

(0006212)
patrick   
2016-06-22 08:38   
(edited on: 2016-06-22 08:46)
• In Fig. 2.11, including allocation-clause in a simple-clause-stmt is redundant, since it is already included in simple-clause.

Yes, and there is the same kind of thing with exits-clause. Fig. 2.11 and 2.22 will be fixed.

(0006213)
patrick   
2016-06-22 11:25   
• 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.

Yes, and that is not allowed by frama-c kernel (except with for prefixes!).
There is also the same kind of thing for loop-annot.

In practice,
- the frama-c kernel will be modified to reject a completely empty set of clauses even after 'for' prefixes.
- the grammar rules will not be modified (since they are easy to read like that), but a footnote will be added.
(0006238)
patrick   
2016-07-22 08:05   
(edited on: 2016-07-22 08:08)
• There is no grammar for the \at, labelName

The grammar will be extended.

(0006239)
patrick   
2016-07-22 08:21   
(edited on: 2016-07-22 08:37)
• There is no grammar for module

The grammar for module definition and use is still open (liknked to the WHY3 presentation done at Frama-C day 2016). The word 'Experimental' can be mentionned at the begining of the section.

(0006240)
patrick   
2016-07-22 08:25   
@David, can you give more inputs about these two issues:
• There is no grammar for ::, open statement constructs
(0006822)
patrick   
2019-07-17 10:59   
Note: issues related to ACSL has to be reported at https://github.com/acsl-language/acsl/issues [^]