ID0002115: **This issue was created automatically from Mantis Issue 2115. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0002115 | 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 a set of typos and grammatical errors I noted on a recent read of most of the ACSL 1.9 manual. None of these affect technical correctness - just the flow of the English. I put them here simply to be helpful. Do what you like with them. If you like, I am happy to edit them into a version-controlled copy of the document source myself, if you would like. Typos & Grammatical corrections p.13: "used in position of a term or a predicate" -> "used in the position of a term or a predicate" p. 17: "name x for expression e1 which can be used in" -> "name x for expression e1 ; x can then be used in" p. 17: "for readibility purposes" -> "for readability purposes" p. 20, near end: "specified if divisor is" -> "specified if the divisor is" p. 23: "involve any rounding nor overflow" -> "involve any rounding or overflow" p. 23: "values which do not naturally" -> "values that do not naturally" p. 23: "mode in C programs) If the source real number" -> "mode in C programs). If the source real number" (period added) p. 26: "pointers can only refers" -> "pointers can only refer" p. 27: "functional update of an union. For an object of an union" -> "functional update of a union. For an object of a union" p. 27: "Then equality amounts the recursively check equality of fields." -> "Then equality amounts to recursively checking equality of fields." p. 27: "C aggregates types" -> "C aggregate types" p. 28: "only for arrays that lies in C" -> "only for arrays that lie in C" p. 28: Did you intentionally omit the section on string literals? (2.2.8) p. 29, last line: "Thus, \old construct is useless" -> "Thus, the \old construct is useless" (2 changes) p. 30: "denotes the effective parameter of isqrt calls which" -> "denotes the effective parameter of isqrt calls, which" (comma expected here) p. 30: "in the pre-state than in the post-state" -> "in the pre-state as in the post-state" p. 33: "If such a condition is seeked," -> "If such a condition is desired," p. 34: "which are also usefull for \separated predicate" -> "that are also useful for the \separated predicate" (three changes) p. 38: "that are not member of L." -> "that are not members of L." p. 38: "is similar as above" -> "is similar to the above" p. 38, Remarks: "locations that are not member of L" -> "locations that are not members of L" p.43, last line: "but without decreases clause" -> "but without a decreases clause" p. 44: "the begining of the annoted statement" -> "the beginning of the annotated statement" (two changes) p. 47, last line: "These declarations follows the" -> "These declarations follow the" p. 49, Example 2.39: "The following introduce" -> "The following introduces" p. 50: "was also bases on definite Horn clauses thus consistent" -> "was also based on definite Horn clauses, and is thus consistent" (2 changes) p. 51: "there is no syntactic conditions which would" -> "there is no syntactic conditions that would" p. 52, Example 2.43: "Function that sums the element" -> "Function that sums the elements" p. 54: "C types and logic types arguments" -> "C type and logic type arguments" or "C types and logic types as arguments" p. 54: "Such an hybrid predicate" -> "Such a hybrid predicate" p. 54: "an hybrid function" -> "a hybrid function" p. 55, Example 2.46: "This second example defines a predicate which indicates" -> "This second example defines a predicate that indicates" p. 55, Example 2.46: "one of the post condition" -> "one of the post conditions" p. 55, "Logic declaration can be augmented" -> "Logic declarations can be augmented" p. 55: "of an hybrid" -> "of a hybrid" p. 56: "that is the set of memory locations which it depends on. From such an information" -> "that is, the set of memory locations that it depends on. From such information" (3 changes) p. 57: "Grammar for terms and predicates" -> "The grammar for terms and predicates" p. 57, at end of page: '(when the allocation succeed)" -> "(when the allocation succeeds)" p. 58, at top of page: "All of them takes" -> "All of them take" or "Each of them takes" p. 58, near bottom of page: "if there is no alignment constraints" -> "if there are no alignment constraints" p. 59: "in the post-state than in the pre-state" -> "in the post-state as in the pre-state" p. 61: "none of the two allocation clauses" -> "neither of the two allocation clauses" p. 61: "That is equivalent to give allocates \nothing" -> "That is equivalent to stating allocates \nothing" p. 63: "A loop-clause without allocation clause implicitly contents loop allocates \nothing" -> "A loop-clause without an allocation clause implicitly states loop allocates \nothing" (2 changes) p. 64: "since union is made with a" -> "since the arguments of union are a" p. 64: "accordingly to" -> "according to" p. 65: "abrupt clause of a statement contracts" -> "abrupt clause of statement contracts" p. 65: "e.g the value" -> "e.g. the value" (period added) p. 72, near end: "semantical restrictions" -> "semantic restrictions" p. 73: "execution This implies several conditions, including e.g:" -> "execution. This implies several conditions, including e.g.:" (two periods added) p. 73: "Body of a ghost function is ghost code, hence do not modify" -> "The body of a ghost function is ghost code, and hence may not modify" p. 74: "so as the ghost field of structures" -> "as do the ghost fields of structures" p. 79: "functions and predicate over" -> "functions and predicates over" p. 80, near end: "the pointer in argument is" -> "the pointer in the argument is" p. 83: "in the future, and remain open" -> "in the future and remain open" (no comma) p. 85: "The set of pure expression is a subset" -> "The set of pure expressions is a subset"