diff --git a/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class new file mode 100644 index 00000000000..3ad4e6ebe86 Binary files /dev/null and b/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.class differ diff --git a/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException1/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..7988e85700e --- /dev/null +++ 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 new file mode 100644 index 00000000000..e8f7c941fd4 --- /dev/null +++ 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 new file mode 100644 index 00000000000..3ac62d1ede5 Binary files /dev/null and b/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.class differ diff --git a/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException2/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..0c83bf9a409 --- /dev/null +++ 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 new file mode 100644 index 00000000000..00820d86c6e --- /dev/null +++ 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 new file mode 100644 index 00000000000..21c451e02f3 Binary files /dev/null and b/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.class differ diff --git a/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException3/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..dfe7b031288 --- /dev/null +++ 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 new file mode 100644 index 00000000000..e8f7c941fd4 --- /dev/null +++ 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 new file mode 100644 index 00000000000..a4723d1d652 Binary files /dev/null and b/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.class differ diff --git a/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException4/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..1e811e417f8 --- /dev/null +++ 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 new file mode 100644 index 00000000000..00820d86c6e --- /dev/null +++ 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 new file mode 100644 index 00000000000..813391d04af Binary files /dev/null and b/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.class differ diff --git a/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException5/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..d32299a427f --- /dev/null +++ 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 new file mode 100644 index 00000000000..d57ec32a9a9 --- /dev/null +++ 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 new file mode 100644 index 00000000000..fdcb29ad252 Binary files /dev/null and b/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.class differ diff --git a/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException6/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..281f868b3e6 --- /dev/null +++ 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 new file mode 100644 index 00000000000..8cab5f69869 --- /dev/null +++ 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