Merge pull request #506 from cristina-david/exception-handling

Java exception handling

Author: Daniel Kroening

regression/cbmc-java/NullPointer3/NullPointer3.class

@@ -4,5 +4,4 @@ public static void main(String[] args)
   {
     throw null; // NULL pointer dereference
   }
-
 }

regression/cbmc-java/NullPointer3/NullPointer3.java

@@ -1,9 +1,9 @@
 CORE
 NullPointer3.class
---pointer-check --stop-on-fail
+--pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^  file NullPointer3.java line 5 function java::NullPointer3.main:\(\[Ljava/lang/String;\)V bytecode_index 1$
+^.*Throw null: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/NullPointer3/test.desc

@@ -0,0 +1,10 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file test.java line 26 function.*: FAILURE$
+\*\* 1 of 9 failed \(2 iterations\)$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/exceptions1/A.class

@@ -0,0 +1,30 @@
+class A extends Throwable {}
+class B extends A {}
+class C extends B {}
+class D extends C {}
+
+public class test {
+ public static void main (String arg[]) {
+   try {
+     D d = new D();
+     C c = new C();
+     B b = new B();
+     A a = new A();
+     A e = a;
+     throw e;
+   }
+   catch(D exc) {
+     assert false;
+   }
+   catch(C exc) {
+     assert false;
+   }
+   catch(B exc) {
+     assert false;
+   }
+   catch(A exc) {
+     assert false;
+   }  
+ }
+}
+

regression/cbmc-java/exceptions1/B.class

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

regression/cbmc-java/exceptions1/C.class

@@ -0,0 +1,25 @@
+class A extends RuntimeException {}
+class B extends A {}
+class C extends B {}
+
+public class test {
+  static void foo() {
+    try {
+      A b = new A();
+      throw b;
+    }
+    catch(A exc) {
+      assert false;
+    }
+  }
+  
+  public static void main (String args[]) {
+    try {
+      A a = new A();
+      foo();
+    }
+    catch(B exc) {
+      assert false;
+    }
+  }
+}

regression/cbmc-java/exceptions1/D.class

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

regression/cbmc-java/exceptions1/test.class

@@ -0,0 +1,39 @@
+class A extends RuntimeException {
+  int i=1;
+};
+
+class B extends A {
+};
+
+public class test {
+  static int foo(int k) {
+    try {
+      if(k==0)
+      {
+	A a = new A();
+	throw a;
+      }
+      else
+      {
+	A b = new A();
+	throw b;
+      }
+	
+    }
+    catch(B exc) {
+      assert exc.i==1;
+    }
+    return 1;
+  }
+
+  
+  public static void main (String args[]) {
+    try {
+      A a = new A();
+      foo(6);
+    }
+    catch(A exc) {
+      assert exc.i==2;
+    }
+  }
+}

regression/cbmc-java/exceptions1/test.desc

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

regression/cbmc-java/exceptions1/test.java

@@ -0,0 +1,27 @@
+class A extends RuntimeException {}
+class B extends A {}
+class C extends B {}
+
+class F {
+  void foo() {
+    try {
+      B b = new B();
+      throw b;
+    }
+    catch(B exc) {
+      assert false;
+    }
+  }
+}
+
+public class test {
+  public static void main (String args[]) {
+    try {
+      F f = new F();
+      f.foo();
+    }
+    catch(B exc) {
+      assert false;
+    }
+  }
+}

regression/cbmc-java/exceptions10/A.class

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

regression/cbmc-java/exceptions10/B.class

@@ -0,0 +1,28 @@
+class A extends RuntimeException {}
+class B extends A {}
+class C extends B {}
+
+class F {
+  void foo() {
+    try {
+      B b = new B();
+      throw b;
+    }
+    catch(B exc) {
+      throw exc;
+    }
+  }
+}
+
+public class test {
+ 
+  public static void main (String args[]) {
+    try {
+      F f = new F();
+      f.foo();
+    }
+    catch(B exc) {
+      assert false;
+    }
+  }
+}

regression/cbmc-java/exceptions10/C.class

@@ -0,0 +1,8 @@
+CORE
+test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/exceptions10/test.class

@@ -0,0 +1,24 @@
+class A extends RuntimeException {}
+class B extends A {}
+class C extends B {}
+
+public class test {
+  public static void main (String args[]) {
+    try {
+      try {
+	C c = new C();
+	A a = new A();
+      }
+      catch(C exc) {
+	assert false;
+      }
+      catch(B exc) {
+	assert false;
+      }
+    }
+    catch(A exc) {
+      assert false;
+    }
+
+  }
+}

regression/cbmc-java/exceptions10/test.desc

@@ -0,0 +1,8 @@
+CORE
+test.class
+--function test.translate
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/exceptions10/test.java

@@ -0,0 +1,20 @@
+class InetAddress {}
+class InetSocketAddress {}
+
+public class test {
+  public String lookupPtrRecord(InetAddress address) {
+    return "Foo";
+  }
+
+  public InetAddress reverse(InetAddress address) {
+    return address;
+  }
+
+  public void translate(InetAddress address, int i) {
+    try {
+      String domainName = lookupPtrRecord(reverse(address));
+    } catch (Exception e) {
+      assert false;
+    }
+  }
+}

regression/cbmc-java/exceptions11/A.class

@@ -0,0 +1,9 @@
+CORE
+test.class
+--function test.foo
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file test.java line 18 function.*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/exceptions11/B.class

@@ -0,0 +1,21 @@
+class A extends RuntimeException {}
+class B extends A {}
+class C extends B {}
+
+public class test {
+  static void foo (int x) {
+    try {
+      x++;
+    }
+    catch(A exc) {
+      assert false;
+    }
+
+    try {
+      throw new B();
+    }
+    catch(B exc) {
+      assert false;
+    }
+  }
+}

regression/cbmc-java/exceptions11/test.class

@@ -0,0 +1,23 @@
+class A extends RuntimeException {}
+class B extends A {}
+
+public class Test {
+  void foo()
+  {
+    A a=new A();
+    throw a;
+  }
+  void goo()
+  {
+    try
+    {
+      foo();
+      assert false;
+    }
+    catch(B e)
+    {
+      assert false;
+    } 
+  }
+  
+}

regression/cbmc-java/exceptions11/test.desc

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--function Test.goo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/exceptions11/test.java

@@ -0,0 +1,10 @@
+CORE
+test.class
+
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file test.java line 15 function.*: FAILURE$
+^\*\* 1 of 5 failed \(2 iterations\)$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc-java/exceptions12/A.class

@@ -0,0 +1,18 @@
+class A extends Throwable {}
+class B extends A {}
+class C extends B {}
+
+public class test {
+  public static void main (String args[]) {
+    try {
+      B b = new B();
+      throw b;
+    }
+    catch(C exc) {
+      assert false;
+    }
+    catch(B exc) {
+      assert false;
+    }
+  }
+}

regression/cbmc-java/exceptions12/B.class

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