Peter's comments 2

Remove --function from one of the examples

Author: Joel Allred

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

@@ -167,7 +167,7 @@ from `java.lang.String`, e.g.
   2|
   3| public class ExampleModels {
   4|
-  5|     public static void stringOp() {
+  5|     public static void main(String[] args) {
   6|         StringBuilder sb = new StringBuilder("abcd");
   7|         StringBuilder sb2 = sb.insert(2, "$");
   8|         assert sb2.toString().startsWith("abc");
@@ -178,13 +178,17 @@ from `java.lang.String`, e.g.
 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 --cp <path_to_cbmc>/jbmc/src/java_bytecode/library/core-models.jar:.
 
 will flag this violation (truncated):
 ```c
 [java::tutorial.ExampleModels.stringOp:()V.assertion.1] line 8 assertion: FAILURE
 ```
-Again, the trace shows the string violating the condition in the assertion:
+Also note that when we want the main function of the class to be the entry
+point of the analysis, we can remove the `--function` option.
+
+Again, the trace (when re-running with `--trace`) shows the string violating
+the condition in the assertion:
 ```c
 dynamic_object2={ 'a', 'b', '$', 'c', 'd' }
 ```