Merge pull request #4753 from peterschrammel/jbmc-java-cmdline

Make JBMC commandline 'java' compatible [TG-9888]

Author: peterschrammel

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

@@ -1,5 +1,5 @@
 CORE
-aliasing1.class
+aliasing1
 --taint taint.json
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/janalyzer-taint/taint-aliasing1/test.desc

@@ -1,5 +1,5 @@
 CORE
-basic1.class
+basic1
 --taint taint.json
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/janalyzer-taint/taint-basic1/test.desc

@@ -1,5 +1,5 @@
 CORE
-basic2.class
+basic2
 --taint taint.json
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/janalyzer-taint/taint-basic2/test.desc

@@ -1,5 +1,5 @@
 CORE
-interface1.class
+interface1
 --taint taint.json
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/janalyzer-taint/taint-interface1/test.desc

@@ -1,5 +1,5 @@
 CORE
-interproc1.class
+interproc1
 --taint taint.json
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/janalyzer-taint/taint-interproc1/test.desc

@@ -1,5 +1,5 @@
 KNOWNBUG
-map1.class
+map1
 --taint taint.json
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/janalyzer-taint/taint-map1/test.desc

@@ -1,5 +1,5 @@
 CORE
-Basic1.class
+Basic1
 --location-sensitive --constants --show
 ^EXIT=0$
 ^SIGNAL=0$

jbmc/regression/janalyzer/string-initializer/test.desc

@@ -1,6 +1,6 @@
 CORE
-A.class
-B.class
-^Only one \.class, \.jar or \.gbf file should be directly specified on the command-line
+A
+B
+Please give exactly one class name, and/or use -jar jarfile or --gb goto-binary
 ^EXIT=1$
 ^SIGNAL=0$

jbmc/regression/janalyzer/too-many-args/test.desc

@@ -1,5 +1,5 @@
 CORE
-A.class
+A
 --function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$