Address comments about user documentation

Will be squashed.

Author: petr-bauch

doc/cprover-manual/index.md

@@ -8,7 +8,9 @@
 
 [A Short Tutorial](cbmc/tutorial/),
 [Loop Unwinding](cbmc/unwinding/),
-[Assertion Checking](cbmc/assertions/)
+[Assertion Checking](cbmc/assertions/),
+[Memory Analyzer](cbmc/memory-analyzer/),
+[Program Harness](cbmc/goto-harness/)
 
 ## 4. [Test Suite Generation](test-suite/)
 

doc/cprover-manual/memory-analyzer.md

@@ -3,11 +3,13 @@
 ## Memory Analyzer
 
 The memory analyzer is a front-end for running and querying GDB in order to
-obtain a state of the input program. A common application would be to obtain a
-snapshot of a program under analysis at a particular state of execution. Such a
-snapshot could be useful on its own: to query about values of particular
-variables. Furthermore, since that snapshot is a state of a valid concrete
-execution, it can also be used for subsequent analyses.
+obtain a state of the input program. The GDB is not needed to be executed
+directly but is rather used as a back-end for the memory analysis. A common
+application would be to obtain a snapshot of a program under analysis at a
+particular state of execution. Such a snapshot could be useful on its own: to
+query about values of particular variables. Furthermore, since that snapshot is
+a state of a valid concrete execution, it can also be used for subsequent
+analyses.
 
 ## Usage
 
@@ -16,18 +18,24 @@ debugging symbols and a symbol table information understandable by CBMC, e.g.
 (having `goto-gcc` on the `PATH`):
 
 ```sh
-$ goto-gcc -g -std=c11 input_program.c -o input_program_exe
+$ goto-gcc -g input_program.c -o input_program_exe
 ```
 
 Calling `goto-gcc` instead of simply compiling with `gcc` produces an ELF binary
-with a goto section that contains the goto model (goto program + symbol table).
+with a goto section that contains the goto model (goto program + symbol table)
+[goto-cc-variants](../goto-cc/variants/).
 
-The user can choose to either run GDB from a core-file `--core-file cf` or to a
-break-point `--breakpoint bp` (and only one of those). The tool also expects a
-comma-separated list of symbols to be analysed `--symbols s1, s2, ..`. Given its
-dependence on GDB, `memory-analyzer` is a Unix-only tool. The tool calls `gdb`
-to obtain the snapshot which is why the `-g` option is necessary for the program
-symbols to be visible.
+The memory analyzer supports two workflows to initiate the GDB with user code:
+either to run the code from a core-file or up to a break-point. If the user
+already has a core-file, they can specify it with the option `--core-file cf`.
+If the user knows the point of their program from where they want to run the
+analysis, they can specify it with the option `--breakpoint bp`. Only one of
+core-file/break-point option can be used.
+
+The tool also expects a comma-separated list of symbols to be analysed
+`--symbols s1, s2, ..`. Given its dependence on GDB, `memory-analyzer` is a
+Unix-only tool. The tool calls `gdb` to obtain the snapshot which is why the
+`-g` option is necessary for the program symbols to be visible.
 
 Take for example the following program:
 
@@ -51,7 +59,7 @@ Say we are interested in the evaluation of `array` at the call-site of
 `checkpoint`. We compile the program with
 
 ```sh
-$ goto-gcc -g -std=c11 main.c -o main_exe
+$ goto-gcc -g main.c -o main_exe
 ```
 
 And then we call `memory-analyzer` with:
@@ -60,17 +68,20 @@ And then we call `memory-analyzer` with:
 $ memory-analyzer --breakpoint checkpoint --symbols array main_exe
 ```
 
-to obtain as output:
+to obtain as output the human readable list of values for each requested symbol:
 
 ```
 {
   array = { 1, 4, 3 };
 }
 ```
 
-Finally, to obtain an output in JSON format, e.g. for further analyses by
-`goto-harness` pass the additional option `--json-ui` together with requesting
-the output to be a symbol table by `--symtab-snapshot`.
+The above option is useful for the user and their preliminary analysis but does
+not contain enough information for further computer-based analyses. To that end,
+memory analyzer has an option to request the result to be a snapshot of the
+whole symbol table `--symtab-snapshot`. Finally, to obtain an output in JSON
+format, e.g. for further analyses by `goto-harness` pass the additional option
+`--json-ui`.
 
 ```sh
 $ memory-analyzer --symtab-snapshot --json-ui \