From 396adaf2f55e5d155a1e3710bf88247765fbf91d Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 4 Dec 2017 17:05:50 +0000 Subject: [PATCH 1/9] Fix include statements in java_bytecode_instrument --- src/java_bytecode/java_bytecode_instrument.cpp | 3 ++- src/java_bytecode/java_bytecode_instrument.h | 4 ++++ 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 07f8c4dbb49..85562e55d2c 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" diff --git a/src/java_bytecode/java_bytecode_instrument.h b/src/java_bytecode/java_bytecode_instrument.h index d48e7758611..91c02009ade 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, From 2f7ee602cdc7bffd7eef73b6c2368063dbde68a7 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 4 Dec 2017 17:06:33 +0000 Subject: [PATCH 2/9] Store list of runtime exceptions in new variable The new public variable exception_needed_classes stores a list of Java exception classes that can be introduced by java_bytecode_instrument. These five classes can be generated by a Java program without explicitly using "throw new". --- src/java_bytecode/java_bytecode_instrument.cpp | 9 +++++++++ src/java_bytecode/java_bytecode_instrument.h | 2 ++ 2 files changed, 11 insertions(+) diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 85562e55d2c..a5981a913c5 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -80,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 91c02009ade..cb5102fb49d 100644 --- a/src/java_bytecode/java_bytecode_instrument.h +++ b/src/java_bytecode/java_bytecode_instrument.h @@ -26,4 +26,6 @@ void java_bytecode_instrument( const bool throw_runtime_exceptions, message_handlert &_message_handler); +extern const std::vector exception_needed_classes; + #endif From 4c472e9c8e4ec0a5913e3e9db198cda794351249 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 4 Dec 2017 17:21:31 +0000 Subject: [PATCH 3/9] Always load classes with throw_runtime_exceptions When the command-line option "--throw-runtime-exception" is enabled, the five runtime exception classes ArithmeticException ArrayIndexOutOfBoundsException ClassCastException NegativeArraySizeException NullPointerException should always be loaded. These five classes might appear without an explicit call to "throw new" in the program, and would therefore be ignored by java_class_loader. These changes fix bug TG-774. --- src/java_bytecode/java_bytecode_language.cpp | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) 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= From 41d77f45b8851e3d56ab824e89d156235b906817 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Fri, 1 Dec 2017 18:29:41 +0000 Subject: [PATCH 4/9] Add regression test for ArithmeticException The new regression test checks that an ArithmeticException is correctly caught if the catch block specifies one of its superclasses. --- .../ArithmeticExceptionTest.class | Bin 0 -> 619 bytes .../ArithmeticExceptionTest.java | 11 +++++++++++ .../java/lang/ArithmeticException.class | Bin 0 -> 232 bytes .../java/lang/ArithmeticException.java | 4 ++++ .../java/lang/RuntimeException.class | Bin 0 -> 219 bytes .../java/lang/RuntimeException.java | 4 ++++ .../cbmc-java/ArithmeticException7/test.desc | 9 +++++++++ 7 files changed, 28 insertions(+) create mode 100644 regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.class create mode 100644 regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.java create mode 100644 regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.class create mode 100644 regression/cbmc-java/ArithmeticException7/java/lang/ArithmeticException.java create mode 100644 regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.class create mode 100644 regression/cbmc-java/ArithmeticException7/java/lang/RuntimeException.java create mode 100644 regression/cbmc-java/ArithmeticException7/test.desc diff --git a/regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.class b/regression/cbmc-java/ArithmeticException7/ArithmeticExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..621ed3729b0f22ade9a1335f634bf4892e353be0 GIT binary patch literal 619 zcmZ`$%T60X5Uk!^d(5(aU=lFKyd)050WRF)L?9rC$iTq}34B_wM=-EnquDXyTlfLa zBvOzP3GRGUl%6Hnr)Z>kbXQeZ_q_i3^$cJeD?SRC5tyAo9yNhEAD(^JeaxdFut1nz z4bxO=qXtR3uhOs^%N~Kw3HhcqKh;J^)y5_yeuLVAd&)min=+OdE z;ys@Qi791N_->&cI7|lWZnNUg$DbciZGDG(kICQg&YqBadCXXX%Q(EOPMwv&AM79p zkr@zNyns2zOmRlQ`6f^;acFwvX*-hvrmFd$5cd$?13dQ!T$iWGAY!@H0 G^vAygOn5H< literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..a85ed965b94f14ef8b4039a41f7ab4ddc40b956f GIT binary patch literal 232 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj;aHSel98KQl9}vUk(^pkl9`{Umz7wS$iu+G zz{nF^EX6aJ literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..2f0ac26544c602aa8e73f1ca35724acb4aa9c8a5 GIT binary patch literal 219 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj8dREBl9`+8T9KSuP?DLSr!T}UWDrJ3!ZkA}GB5$11Okje2s8vpvH^LrU_Ju_tJZb~#*JWUb|A?H Q6lMTwU}WF`(o77T0A{Z)TL1t6 literal 0 HcmV?d00001 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 From 379e415b2966eb095ab6aa3cb9a546f7a7f2e029 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Fri, 1 Dec 2017 19:50:37 +0000 Subject: [PATCH 5/9] Add regression test for NullPointerException The new test is similar to NullPointerException2. It checks that a NullPointerException is correctly caught if the catch block specifies one of its superclasses. --- .../cbmc-java/NullPointerException4/A.class | Bin 0 -> 195 bytes .../cbmc-java/NullPointerException4/Test.class | Bin 0 -> 646 bytes .../cbmc-java/NullPointerException4/Test.java | 15 +++++++++++++++ .../java/lang/NullPointerException.class | Bin 0 -> 234 bytes .../java/lang/NullPointerException.java | 4 ++++ .../java/lang/RuntimeException.class | Bin 0 -> 219 bytes .../java/lang/RuntimeException.java | 4 ++++ .../cbmc-java/NullPointerException4/test.desc | 9 +++++++++ 8 files changed, 32 insertions(+) create mode 100644 regression/cbmc-java/NullPointerException4/A.class create mode 100644 regression/cbmc-java/NullPointerException4/Test.class create mode 100644 regression/cbmc-java/NullPointerException4/Test.java create mode 100644 regression/cbmc-java/NullPointerException4/java/lang/NullPointerException.class create mode 100644 regression/cbmc-java/NullPointerException4/java/lang/NullPointerException.java create mode 100644 regression/cbmc-java/NullPointerException4/java/lang/RuntimeException.class create mode 100644 regression/cbmc-java/NullPointerException4/java/lang/RuntimeException.java create mode 100644 regression/cbmc-java/NullPointerException4/test.desc diff --git a/regression/cbmc-java/NullPointerException4/A.class b/regression/cbmc-java/NullPointerException4/A.class new file mode 100644 index 0000000000000000000000000000000000000000..b61ab2d67da432a7763b6cc91df0374a0acd4f2e GIT binary patch literal 195 zcmX^0Z`VEs1_l!bel7-P1|D_>UUmjPMh3=AAogTrV6(~0%Pg^DWMJ0N3}a+qan4Uk zWn|#@$;?ajE6q(xEec6Y$^nXS1?QI*C8xS&f;gNZsl_FFS&3zdJPd3M>_C$o85smX zeEponymWp4q^#8B5(WhZCZLrJ42(d`!oUh;0W|g_AdiWG8vv(99>@Ry literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NullPointerException4/Test.class b/regression/cbmc-java/NullPointerException4/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..2f4ac275014585591a88aa6a30b9da8201b1fd37 GIT binary patch literal 646 zcmZuuOHUI~7(L%~+S{29P+G;d3W|ajOk~4OVkA5glA?Xe&;)nZ~pxK@e9BzmVJ1rduZUX!V?b)vkG%Q@~A63_3;ez z3eN@Ag)mKZl9@rAZkjag^mSJt2ZF+yiB0xSkZUgO3*3!CR|}?ECe|N@#~q#QSuhL7 zp@{`E&CjjF@JqPT598iSJ4;O5dutmf+F2MK?S>~Kyuu5G1zHjm*P{N7gx?+vlSpqH zOX%(CG<##Y0tA>KJisDe((9Oi>uaP>tmyzgN`l(Bw0@gsD@g_k{aHGNR{@$>5|qct zkDWsuW#qlbIcKoWWw>^jdfc?p=fD`Zt5cKc?wuM_WZ#jq! z!+nxpvpj`oe)$S=Zh@HMUbuc_YZ=qLTWAjsn}LS3Ugs|0oT0M&4elvQKau}*g~IQ1 zA{`3)#5p6L2ARMYhfIp1)Jr6M cDEAC*?mJxT^;+ZBtL4kX3Eta8k4EL%e>5s{cK`qY literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..bfd5b1e5a5ccf990d0a5ce8d31c76826ee4a85d0 GIT binary patch literal 234 zcmZury$Zr$47~JLYsFbX!A%|P;wUbnlN3>LZ|jGA(tefFim&A)IQRfQl$dtV#RM+7 zi)?X?#5tF#8lQqo;KG1O=#{+}2kPkklM*^V!KP5TOvKj*eQ5k)8N|tc bj25$Q#Q}442i>Z*&1mr$d_bsi)lmNc*J?C= literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..2f0ac26544c602aa8e73f1ca35724acb4aa9c8a5 GIT binary patch literal 219 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj8dREBl9`+8T9KSuP?DLSr!T}UWDrJ3!ZkA}GB5$11Okje2s8vpvH^LrU_Ju_tJZb~#*JWUb|A?H Q6lMTwU}WF`(o77T0A{Z)TL1t6 literal 0 HcmV?d00001 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 From 200017ad86c4449d31d3ff5be03062f263c395bb Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Fri, 1 Dec 2017 21:37:11 +0000 Subject: [PATCH 6/9] Add test for ArrayIndexOutOfBoundsException The new test is similar to ArrayIndexOutOfBoundsException1. It checks that an ArrayIndexOutOfBoundsException is correctly caught if the catch block specifies one of its superclasses. --- .../ArrayIndexOutOfBoundsExceptionTest.class | Bin 0 -> 642 bytes .../ArrayIndexOutOfBoundsExceptionTest.java | 11 +++++++++++ .../lang/ArrayIndexOutOfBoundsException.class | Bin 0 -> 263 bytes .../java/lang/ArrayIndexOutOfBoundsException.java | 4 ++++ .../java/lang/IndexOutOfBoundsException.class | Bin 0 -> 244 bytes .../java/lang/IndexOutOfBoundsException.java | 4 ++++ .../java/lang/RuntimeException.class | Bin 0 -> 219 bytes .../java/lang/RuntimeException.java | 4 ++++ .../ArrayIndexOutOfBoundsException3/test.desc | 9 +++++++++ 9 files changed, 32 insertions(+) create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.java create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.class create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/ArrayIndexOutOfBoundsException.java create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.class create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/IndexOutOfBoundsException.java create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.class create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException3/java/lang/RuntimeException.java create mode 100644 regression/cbmc-java/ArrayIndexOutOfBoundsException3/test.desc diff --git a/regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class b/regression/cbmc-java/ArrayIndexOutOfBoundsException3/ArrayIndexOutOfBoundsExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..b500a095ac41cfbe1c2e8b734362ae73c37f89a3 GIT binary patch literal 642 zcmah`O;6iE5PcInS;rU%q0sQzQdKG+Qn_#gRRv0=ia-uQNYGw3_7*J!8?Eh%{uTZJ zXIiO91(iEL3U$_$~vK`phH4sO~*QWM{wpB_6hE05-GxPQ^#sIKkX>9XOkH?l{zMj z&wp+n%WrbIE90Z(c4l;Zv}y|n+nEeccH~)+&teGPTG;(Z?zfZNgzBTVRBzUek>5YX zkvebXS?lXYlE+cHbsnlSD{xPx*<0HqzyJc)-tX7T2~dSkX!N1=r}?&wNetoD|Ck{?m4>%VXxPg0cjq=@9 zQRXp!iH{|kWGe8#yC}1cDkFk>dmQ&M!iYd=TcAF~q0yeGm4XHssaJkMTtK*&aGjrU WtiVU!CxMouj8gF4j`6I3$NmCTb^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBF3>{wKkSm~LUl3L+kTH>GPlwX>cQtVohoLW$l znV+YZl~|U@!@$D8%E+JrV(aH5=B4Z7*90^bp%kal42ld)K<9%1BM<_u0FrD#o-CNp ez`&}toq=&9SehM3vH^t|fEpMXIDj-011A75@IS2p literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..07ac2ac49f62e772ff6fc217c0988551758bf695 GIT binary patch literal 244 zcmZ`z&kF%z5Pie`V3E6`!o_@q9aovO`70Xb3%}_^% ge@%io*_6>@R!uozw(p=@y0#fD9)k}EIj$MxKisM~FaQ7m literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..2f0ac26544c602aa8e73f1ca35724acb4aa9c8a5 GIT binary patch literal 219 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj8dREBl9`+8T9KSuP?DLSr!T}UWDrJ3!ZkA}GB5$11Okje2s8vpvH^LrU_Ju_tJZb~#*JWUb|A?H Q6lMTwU}WF`(o77T0A{Z)TL1t6 literal 0 HcmV?d00001 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 From 51b1d3814b818c9e954d79b823bd923067603aec Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 4 Dec 2017 09:47:35 +0000 Subject: [PATCH 7/9] Add test for ClassCastException The new test checks that a ClassCastException is correctly caught if the catch block specifies one of its superclasses. --- regression/cbmc-java/ClassCastException3/A.class | Bin 0 -> 197 bytes regression/cbmc-java/ClassCastException3/B.class | Bin 0 -> 197 bytes .../ClassCastExceptionTest.class | Bin 0 -> 642 bytes .../ClassCastExceptionTest.java | 15 +++++++++++++++ .../java/lang/ClassCastException.class | Bin 0 -> 230 bytes .../java/lang/ClassCastException.java | 4 ++++ .../java/lang/RuntimeException.class | Bin 0 -> 219 bytes .../java/lang/RuntimeException.java | 4 ++++ .../cbmc-java/ClassCastException3/test.desc | 9 +++++++++ 9 files changed, 32 insertions(+) create mode 100644 regression/cbmc-java/ClassCastException3/A.class create mode 100644 regression/cbmc-java/ClassCastException3/B.class create mode 100644 regression/cbmc-java/ClassCastException3/ClassCastExceptionTest.class create mode 100644 regression/cbmc-java/ClassCastException3/ClassCastExceptionTest.java create mode 100644 regression/cbmc-java/ClassCastException3/java/lang/ClassCastException.class create mode 100644 regression/cbmc-java/ClassCastException3/java/lang/ClassCastException.java create mode 100644 regression/cbmc-java/ClassCastException3/java/lang/RuntimeException.class create mode 100644 regression/cbmc-java/ClassCastException3/java/lang/RuntimeException.java create mode 100644 regression/cbmc-java/ClassCastException3/test.desc diff --git a/regression/cbmc-java/ClassCastException3/A.class b/regression/cbmc-java/ClassCastException3/A.class new file mode 100644 index 0000000000000000000000000000000000000000..a6f4a62227db5d5645502208b359844e85f1adb3 GIT binary patch literal 197 zcmW-aK@Y(|5QX1pwG`nl5=R{L;wTbnI0*-h`?fZ+O|{Zp;%_-g9Q*)3O3a#M=FR)w zB=h;c-T-Fk1aJ`eX!&RpytyirSrDAj_&{)@@+b-2jVk2!dQM~&izH_f?8|GF%C)kl zALT;pNNBUVr}AP{S;SJCX(n!>4HtC+EeSpA!(0@naF=8yxB3P=0X)MLUpp|H0u)oAZF2qEVi}+erf`t#@Ly4O#?99%$ z3;X@OKL8f!xiH{5=sNHS_EKd^uL#CudLo!XewKv(PGxdmT_ah9B1)OK$Gj?Hxm9%- z2B|2^K$Lp(h~-VIJPT#1=ZUxr4<;-EtqFrV`>Dt-{vk?atT9H5pVvj)e8_I|G-9ub UHG6@c&DvqL8)&e$IknLF1CvN4H2?qr literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/ClassCastException3/ClassCastExceptionTest.class b/regression/cbmc-java/ClassCastException3/ClassCastExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..3bfd144673921c3a6d5aa7283e889d1b5186b3e0 GIT binary patch literal 642 zcmZvZ%}(1u6ot>kA(J=`gzy)j{L_k32{!DC5D;J$C{hp-u$nj{G&DHKc2J*%7hnxY zAQh=)%|jv17)UnA^4#&g_ni5z=lSLDKL9KE<|2<#i7^)`8^;o;M+iWy`~z17YF07Wp;7 zC>VPdA0TdQBl@{!-jWoTFu=WSRlGrmarzOdqX#(EA5Tc{UZYgKMdk|mM@Xi#|8Ej) zftnsFtlJpb^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj?wpfYTgKkYoe$WWjs}23D=@ Z42&DW((FKz4Jgb2)WFEV0i>B2I00-ZGK2sC literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..2f0ac26544c602aa8e73f1ca35724acb4aa9c8a5 GIT binary patch literal 219 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj8dREBl9`+8T9KSuP?DLSr!T}UWDrJ3!ZkA}GB5$11Okje2s8vpvH^LrU_Ju_tJZb~#*JWUb|A?H Q6lMTwU}WF`(o77T0A{Z)TL1t6 literal 0 HcmV?d00001 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 From 9cc319239f675861aac62029613012261a0bf10c Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 4 Dec 2017 10:04:39 +0000 Subject: [PATCH 8/9] Rename test to NegativeArraySizeException1 --- .../NegativeArraySizeExceptionTest.class | Bin .../NegativeArraySizeExceptionTest.java | 0 .../test.desc | 0 3 files changed, 0 insertions(+), 0 deletions(-) rename regression/cbmc-java/{NegativeArraySizeException => NegativeArraySizeException1}/NegativeArraySizeExceptionTest.class (100%) rename regression/cbmc-java/{NegativeArraySizeException => NegativeArraySizeException1}/NegativeArraySizeExceptionTest.java (100%) rename regression/cbmc-java/{NegativeArraySizeException => NegativeArraySizeException1}/test.desc (100%) 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 From 94a6ad421eb0130c6c0536385d27fc31df76fe98 Mon Sep 17 00:00:00 2001 From: Antonia Lechner Date: Mon, 4 Dec 2017 10:08:35 +0000 Subject: [PATCH 9/9] Add test for NegativeArraySizeException The new test is similar to NegativeArraySizeException1 (was called NegativeArraySizeException before the previous commit). It checks that a NegativeArraySizeException is correctly caught if the catch block specifies one of its superclasses. --- .../NegativeArraySizeExceptionTest.class | Bin 0 -> 626 bytes .../NegativeArraySizeExceptionTest.java | 10 ++++++++++ .../java/lang/NegativeArraySizeException.class | Bin 0 -> 246 bytes .../java/lang/NegativeArraySizeException.java | 4 ++++ .../java/lang/RuntimeException.class | Bin 0 -> 219 bytes .../java/lang/RuntimeException.java | 4 ++++ .../NegativeArraySizeException2/test.desc | 9 +++++++++ 7 files changed, 27 insertions(+) create mode 100644 regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.class create mode 100644 regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.java create mode 100644 regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.class create mode 100644 regression/cbmc-java/NegativeArraySizeException2/java/lang/NegativeArraySizeException.java create mode 100644 regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.class create mode 100644 regression/cbmc-java/NegativeArraySizeException2/java/lang/RuntimeException.java create mode 100644 regression/cbmc-java/NegativeArraySizeException2/test.desc diff --git a/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.class b/regression/cbmc-java/NegativeArraySizeException2/NegativeArraySizeExceptionTest.class new file mode 100644 index 0000000000000000000000000000000000000000..c51fb8edf438b2ab1e8e2c4bbfa56750ea7fe302 GIT binary patch literal 626 zcmaJ;O-~y!5Pg%~#L2Qi5@-nDMeQMQfD1RGsu87J0vr+{0Vii;MW$hcyc-1k6#f9` zfYeBBRqp&K#CX*v;({!V?Kf}Uys@8Oe*FcojWrKhlmzB-$e=7R@4>bA1rLi@5?Ch8 ze3nt9Ossoh^i4;y)m3c*of0xt9qRZC!Ktht6WrZiTM?$~I#h@Kikt7zEykIfx5KjnktGnt-g;5`0RV!YsB%9gGVTjQ?>uI?HSWEgq8Oj2(0*6#YaMZ ztZ~#jS3%5^kD=WzKN^qRR*^QUJ?g@f#(hrki=ASP-#p9TK>4!u#U}@3&2yaO+cNLO zdwOFC8dxHxIA#)%xMUi6K3i%NDPF)_>W^2yN3s3@=MEFU;hqeUei|etE<{4JA|<3b zy1cTCS|5V3914swYhR!^#o)}y%yuFH6pERj5O)ynJzVDzjy0BgW6Wx#k@CM<`?E>< F!z+rdeTo18 literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..ec5f9692af7cd578e9103fecc336b22ebc231f16 GIT binary patch literal 246 zcmZ`zu?oUa47}LdYE|3?5y3$nba50xL?`KB#r?HDd z$tAfXpYQ7pV1kAN1CEWFjXJ@aDy@tkEC2ui literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..2f0ac26544c602aa8e73f1ca35724acb4aa9c8a5 GIT binary patch literal 219 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj8dREBl9`+8T9KSuP?DLSr!T}UWDrJ3!ZkA}GB5$11Okje2s8vpvH^LrU_Ju_tJZb~#*JWUb|A?H Q6lMTwU}WF`(o77T0A{Z)TL1t6 literal 0 HcmV?d00001 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