Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002236Frama-CDocumentation > manualspublic2016-06-27 17:152019-07-17 13:27
Assigned Topatrick 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version 
Summary0002236: tset issues in manual "acsl-implementation-Aluminium-20160501.pdf"
Descriptionin fig.2.7 on p.35, the alternative for set comprehension should be
"{ term | binders ..." rather than " tset | binders ... ". The next line's alternative should also use "term" rather than "tset". In the corresponding explanation for set comprehension, probably not "the union of the sets denoted by s" is meant but rather "the set of all terms denoted by s".

When the rule "location-address ::= tset" is shown on p.58 and 79, and "location ::= tset" on p.29 (BTW: I wonder whether both rules should be joined into a single one?), some remark could be given on the semantics of (a singleton containing just) a proper-expression term. For example, "assigns n*n" seems perfectly valid, when "n" is an integer variable - are such clauses forbidden, or do they have a reasonable meaning?

On p.93, in the subsection "Typing rules for sets", rule 4 and 5 appear to deviate from the syntactical form explained at subsection start. There is no \vdash in the antecedent of rule 4, and no comma right of a \vdash in any of the involved 4 lines. In rule 5's antecedent, "b \cup \Lambda" should probably read "b:bool \cup \Lambda". I also didn't understand what "tset \tau" should mean.

In Fig.2.25 on p.72, no initialisation of a model variable is admitted by the grammar (since the rule "parameter ::= type-expr id", appearing on p.49 in Fig.2.12, dosn't allow an initialization), while in example 2.61 on p.73, the model variable "forbidden" is initialized, and apparently by a tset, viz. "\empty".
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
patrick (developer)
2019-07-17 13:27

Issues about ACSL have to to reported at [^]

You might have a look at pull request [^] that seems related to your request.

- Issue History
Date Modified Username Field Change
2016-06-27 17:15 Jochen New Issue
2016-08-03 10:18 signoles Assigned To => patrick
2016-08-03 10:18 signoles Status new => assigned
2019-07-17 13:27 patrick Note Added: 0006825
2019-07-17 13:27 patrick Status assigned => closed
2019-07-17 13:27 patrick Resolution open => fixed

Copyright © 2000 - 2019 MantisBT Team
Powered by Mantis Bugtracker