Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • F frama-c
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
  • Issues 171
    • Issues 171
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Commits
  • Issue Boards
Collapse sidebar
  • pub
  • frama-c
  • Issues
  • #138
Closed
Open
Issue created Jun 27, 2016 by Jochen Burghardt@burghardt

tset issues in manual "acsl-implementation-Aluminium-20160501.pdf"

ID0002236: This issue was created automatically from Mantis Issue 2236. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0002236 Frama-C Documentation > manuals public 2016-06-27 2019-07-17
Reporter Jochen Assigned To patrick Resolution fixed
Priority normal Severity text Reproducibility N/A
Platform - OS - OS Version -
Product Version - Target Version - Fixed in Version -

Description :

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".

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking