Drop java prefix from throw-runtime-exceptions option

The 'java' prefix is not required anymore since JBMC and
CBMC do not share the same command line interface
anymore.

Author: peterschrammel

jbmc/regression/jbmc-strings/StringEquals/test_verify.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 Test.class
---refine-strings --string-max-input-length 5 --string-max-length 100 --unwind 10 --function Test.verify --java-throw-runtime-exceptions
+--refine-strings --string-max-input-length 5 --string-max-length 100 --unwind 10 --function Test.verify --throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 assertion at file Test.java line 60 .* SUCCESS

jbmc/regression/jbmc/ArithmeticException1/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$

jbmc/regression/jbmc/ArithmeticException2/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$

jbmc/regression/jbmc/ArithmeticException3/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$

jbmc/regression/jbmc/ArithmeticException4/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$

jbmc/regression/jbmc/ArithmeticException5/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL

jbmc/regression/jbmc/ArithmeticException6/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions --function ArithmeticExceptionTest.main
+--throw-runtime-exceptions --function ArithmeticExceptionTest.main
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$

jbmc/regression/jbmc/ArithmeticException7/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArithmeticExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$

jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$

jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$

jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc

@@ -1,6 +1,6 @@
 CORE
 ArrayIndexOutOfBoundsExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 8 function.*: FAILURE$

jbmc/regression/jbmc/ClassCastException1/test.desc

@@ -1,6 +1,6 @@
 CORE
 ClassCastExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ClassCastExceptionTest.java line 8 function.*: FAILURE$

jbmc/regression/jbmc/ClassCastException2/test.desc

@@ -1,6 +1,6 @@
 CORE
 ClassCastExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc/ClassCastException3/test.desc

@@ -1,6 +1,6 @@
 CORE
 ClassCastExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file ClassCastExceptionTest.java line 12 function.*: FAILURE$

jbmc/regression/jbmc/NegativeArraySizeException1/test.desc

@@ -1,6 +1,6 @@
 CORE
 NegativeArraySizeExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file NegativeArraySizeExceptionTest.java line 7 function.*: FAILURE$

jbmc/regression/jbmc/NegativeArraySizeException2/test.desc

@@ -1,6 +1,6 @@
 CORE
 NegativeArraySizeExceptionTest.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file NegativeArraySizeExceptionTest.java line 7 function.*: FAILURE$

jbmc/regression/jbmc/NullPointerException2/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file Test.java line 14 function.*: FAILURE$

jbmc/regression/jbmc/NullPointerException3/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file Test.java line 14 function.*: FAILURE$

jbmc/regression/jbmc/NullPointerException4/test.desc

@@ -1,6 +1,6 @@
 CORE
 Test.class
---java-throw-runtime-exceptions
+--throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^.*assertion at file Test.java line 12 function.*: FAILURE$

jbmc/regression/jbmc/cast_null2/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions --function test.main
+--throw-runtime-exceptions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/jbmc/exceptions21/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---function test.f --java-throw-runtime-exceptions
+--function test.f --throw-runtime-exceptions
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL

jbmc/regression/jbmc/exceptions23/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions --function test.main
+--throw-runtime-exceptions --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED

jbmc/regression/jbmc/exceptions24/test.desc

@@ -1,6 +1,6 @@
 CORE
 test.class
---java-throw-runtime-exceptions --function test.main
+--throw-runtime-exceptions --function test.main
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED

jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc

@@ -1,6 +1,6 @@
 CORE
 Main.class
---function Main.main --java-throw-runtime-exceptions
+--function Main.main --throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -45,7 +45,9 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd)
 {
   assume_inputs_non_null=cmd.isset("java-assume-inputs-non-null");
   string_refinement_enabled = !cmd.isset("no-refine-strings");
-  throw_runtime_exceptions=cmd.isset("java-throw-runtime-exceptions");
+  throw_runtime_exceptions =
+    cmd.isset("java-throw-runtime-exceptions") || // will go away
+    cmd.isset("throw-runtime-exceptions");
   assert_uncaught_exceptions = !cmd.isset("disable-uncaught-exception-check");
   throw_assertion_error = cmd.isset("throw-assertion-error");
   threading_support = cmd.isset("java-threading");

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -31,7 +31,8 @@ Author: Daniel Kroening, [email protected]
   "(disable-uncaught-exception-check)" \
   "(throw-assertion-error)" \
   "(java-assume-inputs-non-null)" \
-  "(java-throw-runtime-exceptions)" \
+  "(java-throw-runtime-exceptions)" /* will go a away */ \
+  "(throw-runtime-exceptions)" \
   "(java-max-input-array-length):" /* will go a away */ \
   "(max-nondet-array-length):" \
   "(java-max-input-tree-depth):"   /* will go a away */ \