Feature/new instrumentation runtime exceptions

regression/cbmc-java/ArrayIndexOutOfBoundsException/ArrayIndexOutOfBoundsExceptionTest.java

@@ -0,0 +1,14 @@
+public class ArrayIndexOutOfBoundsExceptionTest {
+    public static void main(String args[]) {
+        try {
+            int[] a=new int[4];
+            a[6]=0;
+            // TODO: fix the bytecode convertion such that there is no need for
+            // an explicit throw in order to convert the handler
+            throw new RuntimeException();
+        }
+        catch(ArrayIndexOutOfBoundsException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ArrayIndexOutOfBoundsException/test.desc

@@ -0,0 +1,9 @@
+CORE
+ArrayIndexOutOfBoundsExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArrayIndexOutOfBoundsExceptionTest.java line 11 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java

@@ -0,0 +1,21 @@
+class A {
+  int i;
+}
+
+class B {
+  int j;
+}
+
+public class ClassCastExceptionTest {
+  public static void main(String args[]) {
+      try {
+          Object x = new Integer(0);
+          String y=(String)x;
+          throw new RuntimeException();
+      }
+      catch (ClassCastException exc) {
+          assert false;
+      }
+
+  }
+}

regression/cbmc-java/ClassCastException1/test.desc

@@ -0,0 +1,9 @@
+CORE
+ClassCastExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ClassCastExceptionTest.java line 17 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java

@@ -0,0 +1,21 @@
+class A {
+  int i;
+}
+
+class B {
+  int j;
+}
+
+public class ClassCastExceptionTest {
+  public static void main(String args[]) {
+      try {
+          Object x = new Integer(0);
+          String y=(String)x;
+          throw new RuntimeException();
+      }
+      catch (ClassCastException exc) {
+          assert false;
+      }
+
+  }
+}

regression/cbmc-java/ClassCastException2/test.desc

@@ -0,0 +1,9 @@
+CORE
+ClassCastExceptionTest.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*Dynamic cast check: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.java

@@ -0,0 +1,11 @@
+public class NegativeArraySizeExceptionTest {
+  public static void main(String args[]) {
+      try {
+          int a[]=new int[-1];
+          throw new RuntimeException();
+      }
+      catch (NegativeArraySizeException exc) {
+          assert false;
+      }
+  }
+}

regression/cbmc-java/NegativeArraySizeException/test.desc

@@ -0,0 +1,9 @@
+CORE
+NegativeArraySizeExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file NegativeArraySizeExceptionTest.java line 8 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/NullPointerException2/Test.java

@@ -0,0 +1,18 @@
+class B extends RuntimeException {}
+
+class A {
+    int i;
+}
+
+public class Test {
+    public static void main(String args[]) {
+        A a=null;
+        try {
+            int i=a.i;
+            throw new B();
+        }
+        catch (NullPointerException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/NullPointerException2/test.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file Test.java line 15 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/NullPointerException3/Test.java

@@ -0,0 +1,18 @@
+class B extends RuntimeException {}
+
+class A {
+    int i;
+}
+
+public class Test {
+    public static void main(String args[]) {
+        A a=null;
+        try {
+            int i=a.i;
+            throw new B();
+        }
+        catch (NullPointerException exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/NullPointerException3/test.desc

@@ -0,0 +1,9 @@
+CORE
+Test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*reference is null in \*a: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/cbmc/cbmc_parse_options.cpp

@@ -1166,6 +1166,7 @@ void cbmc_parse_optionst::help()
     // NOLINTNEXTLINE(whitespace/line_length)
     " --java-max-vla-length        limit the length of user-code-created arrays\n"
     // NOLINTNEXTLINE(whitespace/line_length)
+    " --java-throw-runtime-exceptions Throw runtime exceptions when necessary"
     " --java-cp-include-files      regexp or JSON list of files to load (with '@' prefix)\n"
     " --java-unwind-enum-static    try to unwind loops in static initialization of enums\n"
     "\n"

src/cbmc/cbmc_parse_options.h

@@ -61,6 +61,7 @@ class optionst;
   "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \
   "(graphml-witness):" \
   "(java-max-vla-length):(java-unwind-enum-static)" \
+  "(java-throw-runtime-exceptions)" \
   "(java-cp-include-files):" \
   "(localize-faults)(localize-faults-method):" \
   "(lazy-methods)" \