Frama-C Bug Tracking System - Frama-C
View Issue Details
0002236Frama-CDocumentation > manualspublic2016-06-27 17:152019-07-17 13:27
0002236: tset issues in manual "acsl-implementation-Aluminium-20160501.pdf"
in 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".
No tags attached.
Issue History
2016-06-27 17:15JochenNew Issue
2016-08-03 10:18signolesAssigned To => patrick
2016-08-03 10:18signolesStatusnew => assigned
2019-07-17 13:27patrickNote Added: 0006825
2019-07-17 13:27patrickStatusassigned => closed
2019-07-17 13:27patrickResolutionopen => fixed

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.