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 168
    • Issues 168
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 0
    • Merge requests 0
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Container Registry
    • Model experiments
  • 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
  • #549
Closed
Open
Issue created May 05, 2015 by David Cok@cok

ACSL manual:issues affecting technical correctness or understanding

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


Id Project Category View Due Date Updated
ID0002114 Frama-C Documentation > ACSL public 2015-05-05 2016-01-26
Reporter dcok@grammatech.com Assigned To patrick Resolution fixed
Priority normal Severity minor Reproducibility have not tried
Platform - OS - OS Version -
Product Version Frama-C Sodium Target Version Frama-C Magnesium Fixed in Version Frama-C Magnesium

Description :

These are issues affecting technical correctness or understanding that I encountered in a recent read through of the ACSL 1.9 manual.

p. 27: There are extraneous { delimiters in the example.

p. 51/52, Example 2.42: Either line 3 of the example should have ? (n-1) :" instead of "? n :" or the explanation should be corrected.

p. 56, Example 2.47: "modifies t[k]" -> "only modifies t[k]"

p. 57: "where the file list.acsl contains logic definitions" -> "where the file List.acsl contains logic definitions" - at least I presume the name of the file must be a case-senstive match to the name of the module

p. 58: "\valid {L}(p) <==> \valid{L}(((char *)p)+(0..sizeof(*p)))" should be "\valid {L}(p) <==> \valid{L}(((char *)p)+(0..sizeof(*p)-1))" and similarly for \valid_read

p. 71, Example 2.59: These specs allow forbidden to have more values than the union of {\result} and \old(forbidden)

p. 72: In "It is however possible to write multi-line annotations for ghost code. These annotations are enclosed between /@ and @/. As in normal annotations, @s at the beginning of a line and at the end of the comment (before the final @/) are considered as blank." the /@ and @/ should be /@ and @/

Steps To Reproduce :

Read the documentation

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