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