Drop java prefix from throw-runtime-exceptions option

peterschrammel · peterschrammel · commit 0a10bf372d96 · 2018-07-08T22:04:41.000+01:00
The 'java' prefix is not required anymore since JBMC and
CBMC do not share the same command line interface
anymore.
diff --git a/jbmc/regression/jbmc-strings/StringEquals/test_verify.desc b/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
diff --git a/jbmc/regression/jbmc/ArithmeticException1/test.desc b/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$
diff --git a/jbmc/regression/jbmc/ArithmeticException2/test.desc b/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$
diff --git a/jbmc/regression/jbmc/ArithmeticException3/test.desc b/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$
diff --git a/jbmc/regression/jbmc/ArithmeticException4/test.desc b/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$
diff --git a/jbmc/regression/jbmc/ArithmeticException5/test.desc b/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
diff --git a/jbmc/regression/jbmc/ArithmeticException6/test.desc b/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$
diff --git a/jbmc/regression/jbmc/ArithmeticException7/test.desc b/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$
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException1/test.desc b/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$
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException2/test.desc b/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$
diff --git a/jbmc/regression/jbmc/ArrayIndexOutOfBoundsException3/test.desc b/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$
diff --git a/jbmc/regression/jbmc/ClassCastException1/test.desc b/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$
diff --git a/jbmc/regression/jbmc/ClassCastException2/test.desc b/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$
diff --git a/jbmc/regression/jbmc/ClassCastException3/test.desc b/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$
diff --git a/jbmc/regression/jbmc/NegativeArraySizeException1/test.desc b/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$
diff --git a/jbmc/regression/jbmc/NegativeArraySizeException2/test.desc b/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$
diff --git a/jbmc/regression/jbmc/NullPointerException2/test.desc b/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$
diff --git a/jbmc/regression/jbmc/NullPointerException3/test.desc b/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$
diff --git a/jbmc/regression/jbmc/NullPointerException4/test.desc b/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$
diff --git a/jbmc/regression/jbmc/cast_null2/test.desc b/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$
diff --git a/jbmc/regression/jbmc/exceptions21/test.desc b/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
diff --git a/jbmc/regression/jbmc/exceptions23/test.desc b/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
diff --git a/jbmc/regression/jbmc/exceptions24/test.desc b/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
diff --git a/jbmc/regression/jbmc/no-main-int-array-maybe-null1/test.desc b/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$
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp
@@ -46,7 +46,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");
diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h
@@ -31,7 +31,8 @@ Author: Daniel Kroening, kroening@kroening.com
   "(disable-uncaught-exception-check)" \
   "(throw-assertion-error)" \
   "(java-assume-inputs-non-null)" \
-  "(java-throw-runtime-exceptions)" \
+  "(java-throw-runtime-exceptions)" /* will go away */ \
+  "(throw-runtime-exceptions)" \
   "(java-max-input-array-length):" /* will go away */ \
   "(max-nondet-array-length):" \
   "(java-max-input-tree-depth):"   /* will go away */ \
@@ -52,7 +53,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "                                  at the location of the assert statement\n"                  /* NOLINT(*) */ \
   " --java-assume-inputs-non-null    never initialize reference-typed parameter to the\n"        /* NOLINT(*) */ \
   "                                  entry point with null\n"                                    /* NOLINT(*) */ \
-  " --java-throw-runtime-exceptions  make implicit runtime exceptions explicit\n"                /* NOLINT(*) */ \
+  " --throw-runtime-exceptions       make implicit runtime exceptions explicit\n"                /* NOLINT(*) */ \
   " --max-nondet-array-length N      limit nondet (e.g. input) array size to <= N\n"                           /* NOLINT(*) */ \
   " --max-nondet-tree-depth N        limit size of nondet (e.g. input) object tree;\n" /* NOLINT(*) */ \
   "                                  at level N references are set to null\n" /* NOLINT(*) */ \
