2021-03-03 04:10 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002115Frama-CDocumentation > ACSLpublic2016-01-26 08:52
Assigned Topatrick 
PrioritynormalSeverityminorReproducibilityhave not tried
Product VersionFrama-C Sodium 
Target VersionFrama-C MagnesiumFixed in VersionFrama-C Magnesium 
Summary0002115: Typos and Grammatical corrections for the ACSL 1.9 manual
DescriptionThese 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"
TagsNo tags attached.
Attached Files




signoles (manager)

Thanks a lot for your so careful reading. We will fix them in the next public release.


signoles (manager)

Fixed, except the question about string literals (2.2.8).


patrick (developer)

Removing section bout string literals (2.2.8)

-Issue History
Date Modified Username Field Change
2015-05-05 17:36 dcok@grammatech.com New Issue
2015-05-05 17:36 dcok@grammatech.com Status new => assigned
2015-05-05 17:36 dcok@grammatech.com Assigned To => signoles
2015-05-05 17:43 signoles Note Added: 0005912
2015-05-05 17:43 signoles Assigned To signoles => virgile
2015-05-05 17:43 signoles Target Version => Frama-C Magnesium
2015-05-12 13:26 signoles Assigned To virgile => maroneze
2015-06-09 16:56 signoles Assigned To maroneze => virgile
2015-06-09 16:56 signoles Note Added: 0005937
2015-09-04 10:57 bobot Assigned To virgile => patrick
2015-09-07 13:45 patrick Note Added: 0006025
2015-09-07 13:45 patrick Status assigned => resolved
2015-09-07 13:45 patrick Resolution open => fixed
2016-01-26 08:51 signoles Fixed in Version => Frama-C Magnesium
2016-01-26 08:52 signoles Status resolved => closed
2016-06-21 14:11 signoles Category Documentation => Documentation > ACSL
+Issue History