Merge pull request #1096 from cristina-david/feature/consider-implicit-exceptions-when-building-cfg

Consider Java implicit exceptions when building the CFG

Author: smowton

regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.class

@@ -3,7 +3,6 @@ public static void main(String args[]) {
       try {
           int[] a=new int[4];
           a[4]=0;
-          throw new RuntimeException();
       }
       catch (ArrayIndexOutOfBoundsException exc) {
           assert false;

regression/cbmc-java/ArrayIndexOutOfBoundsException1/ArrayIndexOutOfBoundsExceptionTest.java

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

regression/cbmc-java/ArrayIndexOutOfBoundsException1/test.desc

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

regression/cbmc-java/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.class

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

regression/cbmc-java/ArrayIndexOutOfBoundsException2/ArrayIndexOutOfBoundsExceptionTest.java

@@ -3,7 +3,6 @@ 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/ArrayIndexOutOfBoundsException2/test.desc

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

regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.class

@@ -9,9 +9,6 @@ public static void main(String args[]) {
       try {
           A c = new C();
           B b = (B)c;
-          // TODO: an explicit throw is currently needed in order
-          // for CBMC to convert the exception handler
-          throw new RuntimeException();
       }
       catch (ClassCastException exc) {
           assert false;

regression/cbmc-java/ClassCastException1/ClassCastExceptionTest.java

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

regression/cbmc-java/ClassCastException1/test.desc

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

regression/cbmc-java/ClassCastException2/ClassCastExceptionTest.java

@@ -9,9 +9,6 @@ public static void main(String args[]) {
         A a=null;
         try {
             a.i=0;
-            // TODO: an explicit throw is currently needed in order
-            // for CBMC to convert the exception handler
-            throw new B();
         }
         catch (NullPointerException exc) {
             assert false;

regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.class

@@ -3,7 +3,7 @@ Test.class
 --java-throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
-^.*assertion at file Test.java line 17 function.*: FAILURE$
+^.*assertion at file Test.java line 14 function.*: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.java

@@ -9,9 +9,6 @@ public static void main(String args[]) {
         A a=null;
         try {
             int i=a.i;
-            // TODO: an explicit throw is currently needed in order
-            // for CBMC to convert the exception handler
-            throw new B();
         }
         catch (NullPointerException exc) {
             assert false;

regression/cbmc-java/NegativeArraySizeException/test.desc

@@ -3,7 +3,7 @@ Test.class
 --java-throw-runtime-exceptions
 ^EXIT=10$
 ^SIGNAL=0$
-^.*assertion at file Test.java line 17 function.*: FAILURE$
+^.*assertion at file Test.java line 14 function.*: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/NullPointerException2/Test.class

@@ -1046,6 +1046,13 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
 
     if(i_it->statement=="athrow" ||
+       i_it->statement=="putfield" ||
+       i_it->statement=="getfield" ||
+       i_it->statement=="checkcast" ||
+       i_it->statement=="newarray" ||
+       i_it->statement=="anewarray" ||
+       i_it->statement==patternt("?astore") ||
+       i_it->statement==patternt("?aload") ||
        i_it->statement=="invokestatic" ||
        i_it->statement=="invokevirtual" ||
        i_it->statement=="invokespecial" ||