From d0a844bd3538d1a6f8f989a47525269d8dd00c9c Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 7 Nov 2017 15:31:42 +0000 Subject: [PATCH] Assert denominator non-zero when Java runtime exceptions are disabled All the other Java-instrument checks are presented as exceptions when enabled or as assertions when exceptions are disabled; ArithmeticException is uniquely not checked. This adds an assertion to match the other cases. --- .../cbmc-java/divide_by_zero/DivideByZero.class | Bin 0 -> 284 bytes .../cbmc-java/divide_by_zero/DivideByZero.java | 6 ++++++ regression/cbmc-java/divide_by_zero/test.desc | 9 +++++++++ src/java_bytecode/java_bytecode_instrument.cpp | 8 ++++++-- 4 files changed, 21 insertions(+), 2 deletions(-) create mode 100644 regression/cbmc-java/divide_by_zero/DivideByZero.class create mode 100644 regression/cbmc-java/divide_by_zero/DivideByZero.java create mode 100644 regression/cbmc-java/divide_by_zero/test.desc diff --git a/regression/cbmc-java/divide_by_zero/DivideByZero.class b/regression/cbmc-java/divide_by_zero/DivideByZero.class new file mode 100644 index 0000000000000000000000000000000000000000..04eeb36fc8f96e5aa666868e256685c08aa449e7 GIT binary patch literal 284 zcmYk0J!=9%5Qg8mPdzVwG&W+9?qZ>hoti?$O0-Z?Xtk${teksroI-w9D#5}ZkRKJC z)qpO{$IiU-%>4dct^m5I1h5hMc=J&vczvZ+{zVA^7aQdy!B?f$brU{t*ScUkw_`;HfU( P(Kh!To;K)!85T-6HtR7) literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/divide_by_zero/DivideByZero.java b/regression/cbmc-java/divide_by_zero/DivideByZero.java new file mode 100644 index 00000000000..816be580ab9 --- /dev/null +++ b/regression/cbmc-java/divide_by_zero/DivideByZero.java @@ -0,0 +1,6 @@ +public class DivideByZero { + public static void main(String args[]) { + int i=0; + int j=10/i; + } +} diff --git a/regression/cbmc-java/divide_by_zero/test.desc b/regression/cbmc-java/divide_by_zero/test.desc new file mode 100644 index 00000000000..8b37d5b8064 --- /dev/null +++ b/regression/cbmc-java/divide_by_zero/test.desc @@ -0,0 +1,9 @@ +CORE +DivideByZero.class + +^EXIT=10$ +^SIGNAL=0$ +Denominator should be nonzero: FAILURE +^VERIFICATION FAILED +-- +^warning: ignoring diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 66f62e6ff78..909b839d8be 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -143,7 +143,7 @@ codet java_bytecode_instrumentt::throw_exception( /// flag is set. /// \return Based on the value of the flag `throw_runtime_exceptions`, /// it returns code that either throws an ArithmeticException -/// or is a skip +/// or asserts a nonzero denominator. codet java_bytecode_instrumentt::check_arithmetic_exception( const exprt &denominator, const source_locationt &original_loc) @@ -157,7 +157,11 @@ codet java_bytecode_instrumentt::check_arithmetic_exception( original_loc, "java.lang.ArithmeticException"); - return code_skipt(); + code_assertt ret(binary_relation_exprt(denominator, ID_notequal, zero)); + ret.add_source_location()=original_loc; + ret.add_source_location().set_comment("Denominator should be nonzero"); + ret.add_source_location().set_property_class("integer-divide-by-zero"); + return ret; } /// Checks whether the array access array_struct[idx] is out-of-bounds,