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