Merge pull request #1469 from antlechner/antonia/fix/ci_lazy_method_exception_types

Lazy methods: mark JVM-generated exceptions as always available (fixes TG-774)

Author: smowton

regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.class

@@ -0,0 +1,11 @@
+public class ArithmeticExceptionTest {
+    public static void  main(String args[]) {
+        try {
+            int i=0;
+            int j=10/i;
+        }
+        catch(Exception exc) {
+            assert false;
+        }
+    }
+}

regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.java

@@ -0,0 +1,4 @@
+package java.lang;
+
+public class ArithmeticException extends RuntimeException {
+}

regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.class

@@ -0,0 +1,4 @@
+package java.lang;
+
+public class RuntimeException extends Exception {
+}

regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.java

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

regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.class

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