diff --git a/regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.class new file mode 100644 index 00000000000..621ed3729b0 Binary files /dev/null and b/regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.class differ diff --git a/regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.java b/regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.java new file mode 100644 index 00000000000..8a6e3aafa5c --- /dev/null +++ b/regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.java @@ -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; + } + } +} diff --git a/regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.class b/regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.class new file mode 100644 index 00000000000..a85ed965b94 Binary files /dev/null and b/regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.class differ diff --git a/regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.java b/regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.java new file mode 100644 index 00000000000..94fbd04069d --- /dev/null +++ b/regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.java @@ -0,0 +1,4 @@ +package java.lang; + +public class ArithmeticException extends RuntimeException { +} diff --git a/regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.class b/regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.class new file mode 100644 index 00000000000..2f0ac26544c Binary files /dev/null and b/regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.class differ diff --git a/regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.java b/regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.java new file mode 100644 index 00000000000..3be7f777cc0 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.java @@ -0,0 +1,4 @@ +package java.lang; + +public class RuntimeException extends Exception { +} diff --git a/regression/cbmc-java/ArithmeticException7/test.desc b/regression/cbmc-java/ArithmeticException7/test.desc new file mode 100644 index 00000000000..e8f7c941fd4 --- /dev/null +++ b/regression/cbmc-java/ArithmeticException7/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/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class new file mode 100644 index 00000000000..b500a095ac4 Binary files /dev/null and b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class differ diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.java b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.java new file mode 100644 index 00000000000..9e811f491c8 --- /dev/null +++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.java @@ -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; + } + } +} diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class new file mode 100644 index 00000000000..90434074df6 Binary files /dev/null and b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class differ diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.java b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.java new file mode 100644 index 00000000000..30cb3af8c1d --- /dev/null +++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.java @@ -0,0 +1,4 @@ +package java.lang; + +public class ArrayIndexOutOfBoundsException extends IndexOutOfBoundsException { +} diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class new file mode 100644 index 00000000000..07ac2ac49f6 Binary files /dev/null and b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class differ diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.java b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.java new file mode 100644 index 00000000000..6fef2037c41 --- /dev/null +++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.java @@ -0,0 +1,4 @@ +package java.lang; + +public class IndexOutOfBoundsException extends RuntimeException { +} diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class new file mode 100644 index 00000000000..2f0ac26544c Binary files /dev/null and b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class differ diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.java b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.java new file mode 100644 index 00000000000..3be7f777cc0 --- /dev/null +++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.java @@ -0,0 +1,4 @@ +package java.lang; + +public class RuntimeException extends Exception { +} diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException3/test.desc b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/test.desc new file mode 100644 index 00000000000..e6216e07c79 --- /dev/null +++ b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/test.desc @@ -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 diff --git a/regression/cbmc-java/ClassCastException3/A.class b/regression/cbmc-java/ClassCastException3/A.class new file mode 100644 index 00000000000..a6f4a62227d Binary files /dev/null and b/regression/cbmc-java/ClassCastException3/A.class differ diff --git a/regression/cbmc-java/ClassCastException3/B.class b/regression/cbmc-java/ClassCastException3/B.class new file mode 100644 index 00000000000..fec1576ecdd Binary files /dev/null and b/regression/cbmc-java/ClassCastException3/B.class differ diff --git a/regression/cbmc-java/ClassCastException3/ClassCastExceptionTest.class b/regression/cbmc-java/ClassCastException3/ClassCastExceptionTest.class new file mode 100644 index 00000000000..3bfd1446739 Binary files /dev/null and b/regression/cbmc-java/ClassCastException3/ClassCastExceptionTest.class differ diff --git a/regression/cbmc-java/ClassCastException3/ClassCastExceptionTest.java b/regression/cbmc-java/ClassCastException3/ClassCastExceptionTest.java new file mode 100644 index 00000000000..01a692d72ae --- /dev/null +++ b/regression/cbmc-java/ClassCastException3/ClassCastExceptionTest.java @@ -0,0 +1,15 @@ +class A {} + +class B {} + +public class ClassCastExceptionTest { + public static void main(String args[]) { + try { + Object a = new A(); + B b = (B)a; + } + catch (Exception exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/ClassCastException3/java/lang/ClassCastException.class b/regression/cbmc-java/ClassCastException3/java/lang/ClassCastException.class new file mode 100644 index 00000000000..eee83693b89 Binary files /dev/null and b/regression/cbmc-java/ClassCastException3/java/lang/ClassCastException.class differ diff --git a/regression/cbmc-java/ClassCastException3/java/lang/ClassCastException.java b/regression/cbmc-java/ClassCastException3/java/lang/ClassCastException.java new file mode 100644 index 00000000000..9f4bd5d8d86 --- /dev/null +++ b/regression/cbmc-java/ClassCastException3/java/lang/ClassCastException.java @@ -0,0 +1,4 @@ +package java.lang; + +public class ClassCastException extends RuntimeException { +} diff --git a/regression/cbmc-java/ClassCastException3/java/lang/RuntimeException.class b/regression/cbmc-java/ClassCastException3/java/lang/RuntimeException.class new file mode 100644 index 00000000000..2f0ac26544c Binary files /dev/null and b/regression/cbmc-java/ClassCastException3/java/lang/RuntimeException.class differ diff --git a/regression/cbmc-java/ClassCastException3/java/lang/RuntimeException.java b/regression/cbmc-java/ClassCastException3/java/lang/RuntimeException.java new file mode 100644 index 00000000000..3be7f777cc0 --- /dev/null +++ b/regression/cbmc-java/ClassCastException3/java/lang/RuntimeException.java @@ -0,0 +1,4 @@ +package java.lang; + +public class RuntimeException extends Exception { +} diff --git a/regression/cbmc-java/ClassCastException3/test.desc b/regression/cbmc-java/ClassCastException3/test.desc new file mode 100644 index 00000000000..e2188d63898 --- /dev/null +++ b/regression/cbmc-java/ClassCastException3/test.desc @@ -0,0 +1,9 @@ +CORE +ClassCastExceptionTest.class +--java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file ClassCastExceptionTest.java line 12 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.class b/regression/cbmc-java/NegativeArraySizeException1/NegativeArraySizeExceptionTest.class similarity index 100% rename from regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.class rename to regression/cbmc-java/NegativeArraySizeException1/NegativeArraySizeExceptionTest.class diff --git a/regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.java b/regression/cbmc-java/NegativeArraySizeException1/NegativeArraySizeExceptionTest.java similarity index 100% rename from regression/cbmc-java/NegativeArraySizeException/NegativeArraySizeExceptionTest.java rename to regression/cbmc-java/NegativeArraySizeException1/NegativeArraySizeExceptionTest.java diff --git a/regression/cbmc-java/NegativeArraySizeException/test.desc b/regression/cbmc-java/NegativeArraySizeException1/test.desc similarity index 100% rename from regression/cbmc-java/NegativeArraySizeException/test.desc rename to regression/cbmc-java/NegativeArraySizeException1/test.desc diff --git a/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.class b/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.class new file mode 100644 index 00000000000..c51fb8edf43 Binary files /dev/null and b/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.class differ diff --git a/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.java b/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.java new file mode 100644 index 00000000000..b9361f0ed00 --- /dev/null +++ b/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.java @@ -0,0 +1,10 @@ +public class NegativeArraySizeExceptionTest { + public static void main(String args[]) { + try { + int a[]=new int[-1]; + } + catch (Exception exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.class b/regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.class new file mode 100644 index 00000000000..ec5f9692af7 Binary files /dev/null and b/regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.class differ diff --git a/regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.java b/regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.java new file mode 100644 index 00000000000..ec7cea1e756 --- /dev/null +++ b/regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.java @@ -0,0 +1,4 @@ +package java.lang; + +public class NegativeArraySizeException extends RuntimeException { +} diff --git a/regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.class b/regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.class new file mode 100644 index 00000000000..2f0ac26544c Binary files /dev/null and b/regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.class differ diff --git a/regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.java b/regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.java new file mode 100644 index 00000000000..3be7f777cc0 --- /dev/null +++ b/regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.java @@ -0,0 +1,4 @@ +package java.lang; + +public class RuntimeException extends Exception { +} diff --git a/regression/cbmc-java/NegativeArraySizeException2/test.desc b/regression/cbmc-java/NegativeArraySizeException2/test.desc new file mode 100644 index 00000000000..a203a79a628 --- /dev/null +++ b/regression/cbmc-java/NegativeArraySizeException2/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 diff --git a/regression/cbmc-java/NullPointerException4/A.class b/regression/cbmc-java/NullPointerException4/A.class new file mode 100644 index 00000000000..b61ab2d67da Binary files /dev/null and b/regression/cbmc-java/NullPointerException4/A.class differ diff --git a/regression/cbmc-java/NullPointerException4/Test.class b/regression/cbmc-java/NullPointerException4/Test.class new file mode 100644 index 00000000000..2f4ac275014 Binary files /dev/null and b/regression/cbmc-java/NullPointerException4/Test.class differ diff --git a/regression/cbmc-java/NullPointerException4/Test.java b/regression/cbmc-java/NullPointerException4/Test.java new file mode 100644 index 00000000000..bc5b27987b2 --- /dev/null +++ b/regression/cbmc-java/NullPointerException4/Test.java @@ -0,0 +1,15 @@ +class A { + int i; +} + +public class Test { + public static void main(String args[]) { + A a=null; + try { + a.i=0; + } + catch (Exception exc) { + assert false; + } + } +} diff --git a/regression/cbmc-java/NullPointerException4/java/lang/NullPointerException.class b/regression/cbmc-java/NullPointerException4/java/lang/NullPointerException.class new file mode 100644 index 00000000000..bfd5b1e5a5c Binary files /dev/null and b/regression/cbmc-java/NullPointerException4/java/lang/NullPointerException.class differ diff --git a/regression/cbmc-java/NullPointerException4/java/lang/NullPointerException.java b/regression/cbmc-java/NullPointerException4/java/lang/NullPointerException.java new file mode 100644 index 00000000000..9922a45131f --- /dev/null +++ b/regression/cbmc-java/NullPointerException4/java/lang/NullPointerException.java @@ -0,0 +1,4 @@ +package java.lang; + +public class NullPointerException extends RuntimeException { +} diff --git a/regression/cbmc-java/NullPointerException4/java/lang/RuntimeException.class b/regression/cbmc-java/NullPointerException4/java/lang/RuntimeException.class new file mode 100644 index 00000000000..2f0ac26544c Binary files /dev/null and b/regression/cbmc-java/NullPointerException4/java/lang/RuntimeException.class differ diff --git a/regression/cbmc-java/NullPointerException4/java/lang/RuntimeException.java b/regression/cbmc-java/NullPointerException4/java/lang/RuntimeException.java new file mode 100644 index 00000000000..3be7f777cc0 --- /dev/null +++ b/regression/cbmc-java/NullPointerException4/java/lang/RuntimeException.java @@ -0,0 +1,4 @@ +package java.lang; + +public class RuntimeException extends Exception { +} diff --git a/regression/cbmc-java/NullPointerException4/test.desc b/regression/cbmc-java/NullPointerException4/test.desc new file mode 100644 index 00000000000..800755d16bb --- /dev/null +++ b/regression/cbmc-java/NullPointerException4/test.desc @@ -0,0 +1,9 @@ +CORE +Test.class +--java-throw-runtime-exceptions +^EXIT=10$ +^SIGNAL=0$ +^.*assertion at file Test.java line 12 function.*: FAILURE$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 07f8c4dbb49..a5981a913c5 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -8,6 +8,8 @@ Date: June 2017 \*******************************************************************/ +#include "java_bytecode_instrument.h" + #include #include #include @@ -18,7 +20,6 @@ Date: June 2017 #include #include "java_bytecode_convert_class.h" -#include "java_bytecode_instrument.h" #include "java_entry_point.h" #include "java_root_class.h" #include "java_types.h" @@ -79,6 +80,15 @@ class java_bytecode_instrumentt:public messaget }; +const std::vector exception_needed_classes = +{ + "java.lang.ArithmeticException", + "java.lang.ArrayIndexOutOfBoundsException", + "java.lang.ClassCastException", + "java.lang.NegativeArraySizeException", + "java.lang.NullPointerException" +}; + /// Creates a class stub for exc_name and generates a /// conditional GOTO such that exc_name is thrown when /// cond is met. diff --git a/src/java_bytecode/java_bytecode_instrument.h b/src/java_bytecode/java_bytecode_instrument.h index d48e7758611..cb5102fb49d 100644 --- a/src/java_bytecode/java_bytecode_instrument.h +++ b/src/java_bytecode/java_bytecode_instrument.h @@ -11,6 +11,10 @@ Date: June 2017 #ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_INSTRUMENT_H +#include +#include +#include + void java_bytecode_instrument_symbol( symbol_table_baset &symbol_table, symbolt &symbol, @@ -22,4 +26,6 @@ void java_bytecode_instrument( const bool throw_runtime_exceptions, message_handlert &_message_handler); +extern const std::vector exception_needed_classes; + #endif diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index c949b54f211..15ca64a764e 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -61,10 +61,19 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) else lazy_methods_mode=LAZY_METHODS_MODE_EAGER; + if(cmd.isset("java-throw-runtime-exceptions")) + { + throw_runtime_exceptions = true; + java_load_classes.insert( + java_load_classes.end(), + exception_needed_classes.begin(), + exception_needed_classes.end()); + } if(cmd.isset("java-load-class")) { - for(const auto &c : cmd.get_values("java-load-class")) - java_load_classes.push_back(c); + const auto &values = cmd.get_values("java-load-class"); + java_load_classes.insert( + java_load_classes.end(), values.begin(), values.end()); } const std::list &extra_entry_points=