Regression test for ArithmeticException

diffblue · Aug 7, 2017 · fb89e5a · fb89e5a
1 parent 6ed24e5
commit fb89e5a
Show file tree

Hide file tree

Showing 18 changed files with 120 additions and 0 deletions.
diff --git a/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class
diff --git a/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.java
@@ -0,0 +1,11 @@
+public class ArithmeticExceptionTest {
+    public static void  main(String args[]) {
+        try {
+            int i=0;
+            int j=10/i;
+        }
+        catch(ArithmeticException exc) {
+            assert false;
+        }
+    }
+}
diff --git a/regression/cbmc-java/ArithmeticException1/test.desc b/regression/cbmc-java/ArithmeticException1/test.desc
@@ -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
diff --git a/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.class
diff --git a/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.java
@@ -0,0 +1,12 @@
+public class ArithmeticExceptionTest {
+    public static void  main(String args[]) {
+        try {
+            long denom=0;
+            long num=10;
+            long j=num/denom;
+        }
+        catch(ArithmeticException exc) {
+            assert false;
+        }
+    }
+}
diff --git a/regression/cbmc-java/ArithmeticException2/test.desc b/regression/cbmc-java/ArithmeticException2/test.desc
@@ -0,0 +1,9 @@
+CORE
+ArithmeticExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$
+^VERIFICATION FAILED
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.class
diff --git a/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.java
@@ -0,0 +1,11 @@
+public class ArithmeticExceptionTest {
+    public static void  main(String args[]) {
+        try {
+            int i=0;
+            int j=10%i;
+        }
+        catch(ArithmeticException exc) {
+            assert false;
+        }
+    }
+}
diff --git a/regression/cbmc-java/ArithmeticException3/test.desc b/regression/cbmc-java/ArithmeticException3/test.desc
@@ -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
diff --git a/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.class
diff --git a/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.java
@@ -0,0 +1,12 @@
+public class ArithmeticExceptionTest {
+    public static void  main(String args[]) {
+        try {
+          long denom=0;
+          long num=10;
+          long result=num%denom;
+        }
+        catch(ArithmeticException exc) {
+            assert false;
+        }
+    }
+}
diff --git a/regression/cbmc-java/ArithmeticException4/test.desc b/regression/cbmc-java/ArithmeticException4/test.desc
@@ -0,0 +1,9 @@
+CORE
+ArithmeticExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArithmeticExceptionTest.java line 9 function.*: FAILURE$
+^VERIFICATION FAILED
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.class
diff --git a/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.java
@@ -0,0 +1,11 @@
+public class ArithmeticExceptionTest {
+    public static void  main(String args[]) {
+        try {
+            double i=0;
+            double j=10/i;
+        }
+        catch(ArithmeticException exc) {
+            assert false;
+        }
+    }
+}
diff --git a/regression/cbmc-java/ArithmeticException5/test.desc b/regression/cbmc-java/ArithmeticException5/test.desc
@@ -0,0 +1,8 @@
+CORE
+ArithmeticExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL
+--
+^warning: ignoring
diff --git a/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.class
diff --git a/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.java
@@ -0,0 +1,10 @@
+public class ArithmeticExceptionTest {
+    public static void  main(int denom) {
+        try {
+            int j=10/denom;
+        }
+        catch(ArithmeticException exc) {
+            assert false;
+        }
+    }
+}
diff --git a/regression/cbmc-java/ArithmeticException6/test.desc b/regression/cbmc-java/ArithmeticException6/test.desc
@@ -0,0 +1,9 @@
+CORE
+ArithmeticExceptionTest.class
+--java-throw-runtime-exceptions
+^EXIT=10$
+^SIGNAL=0$
+^.*assertion at file ArithmeticExceptionTest.java line 7 function.*: FAILURE$
+^VERIFICATION FAILED
+--
+^warning: ignoring