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