fixup Rename test classes

Author: Joel Allred

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

@@ -22,13 +22,13 @@ features of JBMC, and explore the most useful features.
 
 \subsection jbmc-manual-auto-assert Automatic assertions
 
-Consider the following simplistic `Example1.java` file which we have compiled
-into `Example1.class` and which contains a utility method to query a given
+Consider the following simplistic `ExampleArray.java` file which we have compiled
+into `ExampleArray.class` and which contains a utility method to query a given
 array at a given index:
 ```
 package tutorial;
 
-public class Example1 {
+public class ExampleArray {
 
     public static int query(int[] array, int index) {
         return array[index];
@@ -39,15 +39,15 @@ public class Example1 {
 Now let's run the following command to let JBMC tell us about potential errors
 in our `query` method.
 
-    jbmc Example1.class --function tutorial.Example1.query
+    jbmc ExampleArray.class --function tutorial.ExampleArray.query
 
 
 The output contains the following:
 
-    [java::tutorial.Example1.query:([II)I.null-pointer-exception.1] line 6 Null pointer check: FAILURE
-    [java::tutorial.Example1.query:([II)I.array-index-out-of-bounds-low.1] line 6 Array index should be >= 0: FAILURE
-    [java::tutorial.Example1.query:([II)I.array-index-out-of-bounds-high.1] line 6 Array index should be < length: FAILURE
-    [java::tutorial.Example1.query:([II)I.1] line 6 no uncaught exception: SUCCESS
+    [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
@@ -59,7 +59,7 @@ safe as follows:
 ```
 package tutorial;
 
-public class Example2 {
+public class ExampleArraySafe {
     public static int query(int[] array, int index) {
         if (array == null) {
             return -1;
@@ -75,11 +75,11 @@ public class Example2 {
 then the JBMC automatic assertions become valid, meaning that there is no
 possible inputs (argument values) for which they can be violated:
 
-    [java::tutorial.Example2.query:([II)I.1] line 6 no uncaught exception: SUCCESS
-    [java::tutorial.Example2.query:([II)I.null-pointer-exception.1] line 9 Null pointer check: SUCCESS
-    [java::tutorial.Example2.query:([II)I.null-pointer-exception.2] line 12 Null pointer check: SUCCESS
-    [java::tutorial.Example2.query:([II)I.array-index-out-of-bounds-low.1] line 12 Array index should be >= 0: SUCCESS
-    [java::tutorial.Example2.query:([II)I.array-index-out-of-bounds-high.1] line 12 Array index should be < length: SUCCESS
+    [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
@@ -93,7 +93,7 @@ depends on an input):
 ```
 package tutorial;
 
-public class Example3 {
+public class ExampleUnwind {
 
     public static void doSomething(int inputVal) {
         if (inputVal > 1 && inputVal % 2 == 1) {
@@ -116,7 +116,7 @@ public class Example3 {
 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 Example3.class --function tutorial.Example3.isPrime --unwind 10
+    jbmc ExampleUnwind.class --function tutorial.ExampleUnwind.isPrime --unwind 10
 
 will terminate (with `VERIFICATION SUCCESSFUL`).
 
@@ -128,12 +128,12 @@ 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 Example3.class --function tutorial.Example3.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/Example3.java: FAILURE
+    [...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
@@ -165,7 +165,7 @@ from `java.lang.String`, e.g.
 ```
 package tutorial;
 
-public class Example4 {
+public class ExampleModels {
 
     public static void stringOp() {
         StringBuilder sb = new StringBuilder("abcd");
@@ -178,11 +178,11 @@ public class Example4 {
 The following command line (note that the current directory is also added to
 the classpath):
 
-    jbmc Example4.class --function tutorial.Example4.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.Example4.stringOp:()V.assertion.1] line 8 assertion: FAILURE
+    [java::tutorial.ExampleModels.stringOp:()V.assertion.1] line 8 assertion: FAILURE
 
 Again, the trace shows the string violating the condition in the assertion:
 
@@ -202,7 +202,7 @@ line 11 will be considered as unreachable, and hence the assertion to be valid.
 ```
 package tutorial;
 
-public class Example5 {
+public class ExampleExceptions {
 
     public static int exceptionHandling(String str) {
         int retval = 0;