Merge pull request #5434 from NlightNFotis/fix/doc_misc_fixes

Minor documentation fixes.

Author: NlightNFotis

doc/architectural/background-concepts.md

@@ -467,7 +467,7 @@ One way to understand which functions form basic blocks is to consider the
 successors of each instruction. If we have two instructions A and B, we say
 that B is a *successor* of A if, after executing A, we can execute B without any
 intervening instructions. For instance, in the example above, the loop
-initialization statement `unsigned long int i.1 = 1` is a successor of
+initialization statement `unsigned int i.1 = 1` is a successor of
 `unsigned long fac.1 = 1`. On the other hand, `return fac.1` is not a successor
 of `unsigned long fac.1 = 1`: we always have to execute some other intermediate
 statements to reach the return statement.
@@ -534,7 +534,7 @@ and \ref analyses-specific-analyses.
 
 While control flow graphs are already quite useful for static analysis,
 some techniques benefit from a further transformation to a
-representation know as **static single assignment**, short **SSA**. The
+representation known as **static single assignment**, short **SSA**. The
 point of this step is to ensure that we can talk about the entire history
 of assignments to a given variable. This is achieved by renaming
 variables again: whenever we assign to a variable, we *clone* this
@@ -1218,23 +1218,24 @@ a map that associates both `fac` and `i` to "not 0".
 An abstract domain is a set $D$ (or, if you
 prefer, a data type) with the following properties:
 - There is a function merge that takes two elements of $D$ and returns
-  an element of $D$. This function is associative (merge(x, merge(y,z))
-  = merge(merge(x,y), z)), commutative (merge(x,y) = merge(y,x)) and
-  idempotent (merge(x,x) = x).
-- There is an element bottom of $D$ such that merge(x, bottom) = x.
+  an element of $D$. This function is:
+  * **associative** - `(merge(x, merge(y,z)) = merge(merge(x,y), z))`,
+  * **commutative** - `(merge(x,y) = merge(y,x))` and
+  * **idempotent** `(merge(x,x) = x)`.
+- There is an element bottom of $D$ such that `merge(x, bottom) = x`.
 
 Algebraically speaking, $D$ needs to be a semi-lattice.
 
 For our example, we use the following domain:
 - D contains the elements "bottom" (nothing is known),
   "equals 0", "not 0" and "could be 0".
 
-- merge is defined as follows:
-  merge(bottom, x) = x
-  merge("could be 0", x) = "could be 0"
-  merge(x,x) = x
-  merge("equals 0", "not 0") = "could be 0"
-- bottom is bottom, obviously.
+- `merge` is defined as follows:
+  * `merge(bottom, x)` = `x`
+  * `merge("could be 0", x)` = `"could be 0"`
+  * `merge(x,x) = `x`
+  * `merge("equals 0", "not 0")` = `"could be 0"`
+- `bottom` is bottom, obviously.
 It is easy but tedious to check that all conditions hold.
 
 The second ingredient we need are the **abstract state transformers**.
@@ -1251,7 +1252,7 @@ case, the result is "could be 0".
 
 What if `x` and `y` are both "not 0"? In a mathematically ideal world,
 we would have `x*y` be non-zero as well. But in a C program,
-multiplication could overflow, yielding 0! So, to be correct, we have to
+multiplication could *overflow*, yielding `0`. So, to be correct, we have to
 yield "could be 0" in this case.
 
 Finally, when `x` is bottom, we can just return whatever value we had

doc/architectural/howto.md

@@ -229,7 +229,7 @@ of that particular node:
   - `node.op0().id() == ID_symbol`
   - `node.op0().type().id() == ID_array`
 
-The fact that the `op0()` child has a `symbol` ID menas that you could
+The fact that the `op0()` child has a `symbol` ID means that you could
 cast it to a `symbol_exprt` (which is a subtype of `exprt`) using the
 function `to_symbol_expr`.
 

src/cbmc/README.md

@@ -36,7 +36,7 @@ can be hit or satisfied (or prove that can't be done).
 For example, given an input program
 `f(int x, int y) { assert(x + y % 3 == 1); assert(x % y == 0); }` then goto-
 symex would produce a formula something like
-`F1 + F2 % 3 != 1 OR (F1 + F2 % 3 == 1 AND F1 % F2 != 0), where F-variables
+`F1 + F2 % 3 != 1 OR (F1 + F2 % 3 == 1 AND F1 % F2 != 0)`, where `F`-variables
 are free. The precise expression of that formula depends on CBMC's command-line
 configuration: for some backends it will lower the arithmetic operations into
 bitwise operations; other backends understand arithmetic and so they will remain