Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002187Frama-CDocumentation > ACSLpublic2015-11-23 02:212019-07-17 10:59
Reporterdcok@grammatech.com 
Assigned Topatrick 
PrioritynormalSeveritytextReproducibilityN/A
StatusclosedResolutionwon't fix 
PlatformOSOS Version
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002187: Grammar omissions in 1.9
DescriptionComments 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)
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0006211)
patrick (developer)
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 (developer)
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 (developer)
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 (developer)
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 (developer)
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 (developer)
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 (developer)
2019-07-17 10:59

Note: issues related to ACSL has to be reported at https://github.com/acsl-language/acsl/issues [^]

- Issue History
Date Modified Username Field Change
2015-11-23 02:21 dcok@grammatech.com New Issue
2015-11-23 02:21 dcok@grammatech.com Status new => assigned
2015-11-23 02:21 dcok@grammatech.com Assigned To => signoles
2015-11-23 04:20 signoles Assigned To signoles => maroneze
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
2016-06-21 14:26 signoles Assigned To maroneze => patrick
2016-06-22 08:28 patrick Note Added: 0006211
2016-06-22 08:38 patrick Note Added: 0006212
2016-06-22 08:46 patrick Note Edited: 0006212 View Revisions
2016-06-22 08:56 patrick Note Edited: 0006211 View Revisions
2016-06-22 08:56 patrick Note Edited: 0006211 View Revisions
2016-06-22 11:25 patrick Note Added: 0006213
2016-07-22 08:05 patrick Note Added: 0006238
2016-07-22 08:08 patrick Note Edited: 0006238 View Revisions
2016-07-22 08:21 patrick Note Added: 0006239
2016-07-22 08:25 patrick Note Added: 0006240
2016-07-22 08:37 patrick Note Edited: 0006239 View Revisions
2019-07-17 10:59 patrick Note Added: 0006822
2019-07-17 10:59 patrick Status assigned => closed
2019-07-17 10:59 patrick Resolution open => won't fix


Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker