fixup! cosmetic fixes

Author: Joel Allred

doc/cprover-manual/jbmc-user-manual.md

@@ -39,15 +39,16 @@ public class ExampleArray {
 Now let's run the following command to let JBMC tell us about potential errors
 in our `query` method.
 
-    jbmc ExampleArray.class --function tutorial.ExampleArray.query
+    $ jbmc ExampleArray.class --function tutorial.ExampleArray.query
 
 
 The output contains the following:
-
-    [java::tutorial.ExampleArray.query:([II)I.null-pointer-exception.1] line 6 Null pointer check: FAILURE
-    [java::tutorial.ExampleArray.query:([II)I.array-index-out-of-bounds-low.1] line 6 Array index should be >= 0: FAILURE
-    [java::tutorial.ExampleArray.query:([II)I.array-index-out-of-bounds-high.1] line 6 Array index should be < length: FAILURE
-    [java::tutorial.ExampleArray.query:([II)I.1] line 6 no uncaught exception: SUCCESS
+```c
+[java::tutorial.ExampleArray.query:([II)I.null-pointer-exception.1] line 6 Null pointer check: FAILURE
+[java::tutorial.ExampleArray.query:([II)I.array-index-out-of-bounds-low.1] line 6 Array index should be >= 0: FAILURE
+[java::tutorial.ExampleArray.query:([II)I.array-index-out-of-bounds-high.1] line 6 Array index should be < length: FAILURE
+[java::tutorial.ExampleArray.query:([II)I.1] line 6 no uncaught exception: SUCCESS
+```
 
 Three reported failures spring up:
 1. there is no null pointer check on the array passed as argument
@@ -74,13 +75,13 @@ public class ExampleArraySafe {
 ```
 then the JBMC automatic assertions become valid, meaning that there is no
 possible inputs (argument values) for which they can be violated:
-
-    [java::tutorial.ExampleArraySafe.query:([II)I.1] line 6 no uncaught exception: SUCCESS
-    [java::tutorial.ExampleArraySafe.query:([II)I.null-pointer-exception.1] line 9 Null pointer check: SUCCESS
-    [java::tutorial.ExampleArraySafe.query:([II)I.null-pointer-exception.2] line 12 Null pointer check: SUCCESS
-    [java::tutorial.ExampleArraySafe.query:([II)I.array-index-out-of-bounds-low.1] line 12 Array index should be >= 0: SUCCESS
-    [java::tutorial.ExampleArraySafe.query:([II)I.array-index-out-of-bounds-high.1] line 12 Array index should be < length: SUCCESS
-
+```c
+[java::tutorial.ExampleArraySafe.query:([II)I.1] line 6 no uncaught exception: SUCCESS
+[java::tutorial.ExampleArraySafe.query:([II)I.null-pointer-exception.1] line 9 Null pointer check: SUCCESS
+[java::tutorial.ExampleArraySafe.query:([II)I.null-pointer-exception.2] line 12 Null pointer check: SUCCESS
+[java::tutorial.ExampleArraySafe.query:([II)I.array-index-out-of-bounds-low.1] line 12 Array index should be >= 0: SUCCESS
+[java::tutorial.ExampleArraySafe.query:([II)I.array-index-out-of-bounds-high.1] line 12 Array index should be < length: SUCCESS
+```
 
 \subsection jbmc-manual-unwind Loop unwinding
 
@@ -116,9 +117,10 @@ public class ExampleUnwind {
 To limit the number of times the for-loop is unwound, we use the `--unwind N`
 options, in which case the following call to JBMC:
 
-    jbmc ExampleUnwind.class --function tutorial.ExampleUnwind.isPrime --unwind 10
+    $ jbmc ExampleUnwind.class --function tutorial.ExampleUnwind.isPrime --unwind 10
 
-will terminate (with `VERIFICATION SUCCESSFUL`).
+will terminate correctly. In this case, we will see `VERIFICATION SUCCESSFUL`,
+as no automatic assertions are violated.
 
 
 \subsection jbmc-manual-user-assert User assertions
@@ -128,20 +130,20 @@ JBMC will try do refute. On line 7, we check the assertion that all odd
 numbers greater than 1 are prime. To be sure that this always holds, we run
 JBMC on the example, with a reasonable `unwind` value:
 
-    jbmc ExampleUnwind.class --function tutorial.ExampleUnwind.doSomething --unwind 10
+    $ jbmc ExampleUnwind.class --function tutorial.ExampleUnwind.doSomething --unwind 10
 
 Unsurprisingly JBMC doesn't agree, and prints an assertion failure
 (truncated here for readability):
-
-    [...doSomething:(I)V.assertion.1] line 7 assertion at file tutorial/ExampleUnwind.java: FAILURE
-
+```c
+[...doSomething:(I)V.assertion.1] line 7 assertion at file tutorial/ExampleUnwind.java: FAILURE
+```
 
 Rerunning the analysis with the `--trace` option, the following line appears
 somewhere in the trace output and tells us which input value JBMC found to
 trigger the violation:
-
-    INPUT inputVal: 15
-
+```c
+INPUT inputVal: 15
+```
 The value chosen by JBMC is arbitrary, and could as well be 9
 or 2084569161.
 Note that to see the original parameter names in the trace
@@ -178,16 +180,16 @@ public class ExampleModels {
 The following command line (note that the current directory is also added to
 the classpath):
 
-    jbmc ExampleModels.class --function tutorial.ExampleModels.stringOp --cp <path_to_cbmc>/jbmc/src/java_bytecode/library/core-models.jar:.
+    $ jbmc ExampleModels.class --function tutorial.ExampleModels.stringOp --cp <path_to_cbmc>/jbmc/src/java_bytecode/library/core-models.jar:.
 
 will flag this violation (truncated):
-
-    [java::tutorial.ExampleModels.stringOp:()V.assertion.1] line 8 assertion: FAILURE
-
+```c
+[java::tutorial.ExampleModels.stringOp:()V.assertion.1] line 8 assertion: FAILURE
+```
 Again, the trace shows the string violating the condition in the assertion:
-
-    dynamic_object2={ 'a', 'b', '$', 'c', 'd' }
-
+```c
+dynamic_object2={ 'a', 'b', '$', 'c', 'd' }
+```
 
 \subsection jbmc-manual-exceptions Exceptions
 
@@ -231,5 +233,5 @@ JBMC has a wealth of other options that can either constrain the model (to
 cope with complexity issues), or output more relevant information. The list
 of all available options is printed by running:
 
-    jbmc --help
+    $ jbmc --help