Merge pull request #6941 from tautschnig/feature/goto-analyzer-man-page

Add goto-analyzer man page

Author: tautschnig

doc/cprover-manual/goto-analyzer.md

@@ -85,7 +85,7 @@ a better picture of exactly what is computed.
 : Every property in the program is checked to see whether it is true
 (it always holds), unreachable, false if it is reachable (due to the
 over-approximate analysis, it is not clear if locations are reachable
-or if it is an overapproximation, so this is the best that can be
+or if it is an over-approximation, so this is the best that can be
 achieved) or unknown.  If there are multiple points of execution that
 reach the same location, each will be checked and the answers
 combined, with unknown taking precedence.
@@ -99,8 +99,8 @@ value.  If this makes instructions unreachable (for example if `GOTO`
 can be shown to never be taken) they will be removed.  Removal can be
 deactivated by passing `--no-simplify-slicing`.  In the ideal world
 simplify would be idempotent (i.e. running it a second time would not
-simply anything more than the first).  However there are edge cases
-which are difficult or prohibitatively expensive to handle in the
+simplify anything more than the first).  However there are edge cases
+which are difficult or prohibitively expensive to handle in the
 domain which can result in a second (or more) runs giving
 simplification.  Submitting bug reports for these is helpful but they
 may not be viable to fix.
@@ -284,7 +284,7 @@ element is stored for every entry in the array.
 : This controls the handling of pointers.  The default, `top-bottom` effectively
 ignores pointers, this is OK if they are just read (all reads return
 top) but if they are written then there is the problem that we know
-that a variable is changed but we don't which one, so we have to set
+that a variable is changed but we know don't which one, so we have to set
 the whole domain to top.  `constants` is somewhat misleadingly named as it
 uses an abstract object that tracks a pointer to a single variable.
 This includes the offset within the variable; a stack of field names
@@ -300,7 +300,7 @@ described above.
 variable of union type.
 
 `--vsd-data-dependencies`
-: Wraps each abstract object with a set of locations whether the
+: Wraps each abstract object with a set of locations where the
 variable was last modified.  The set is reset when the variable is
 written and takes the union of the two sides' sets on merge.  This was
 originally intended for `--dependence-graph-vs` but has proved useful
@@ -383,8 +383,8 @@ is visited.  There is not a direct form of program transformation that
 matches this but it is similar to the per-path analysis that symbolic
 execution does.  The scalability and the risk of non-termination if
 `n` is `0` remain the same.  Note that the goto-programs generated by
-various language front-ends have a condition forwards jump to exit the
-loop if the condition fails at the start and a unconditional backwards
+various language front-ends have a conditional forwards jump to exit the
+loop if the condition fails at the start and an unconditional backwards
 jump at the end.  This means that `--branching` can wind up
 distinguishing different loop iterations -- "has not exited for the
 last 3 iterations" rather than "has jumped back to the top 3 times".