Java: make null-pointer and similar checks fatal

These previously used code_assertt, which asserts but then continues -- this
changes them to use assert(condition); assume(condition), which ensures subsequent
code is not executed in conditions which are in practice impossible.

With --java-throw-runtime-exceptions this is irrelevant, as a real exception is raised
and the conditional GOTO guarding the throw has the same effect as the assume.

Author: smowton

regression/cbmc-java/NullPointer3/test.desc

@@ -3,7 +3,7 @@ NullPointer3.class
 --pointer-check
 ^EXIT=10$
 ^SIGNAL=0$
-^.*Throw null: FAILURE$
+^.*Null pointer check: FAILURE$
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring

regression/cbmc-java/repeated_guards/A.class

@@ -0,0 +1,45 @@
+public class Test {
+
+  // In each of these cases a guard is repeated -- either an explicit assertion,
+  // or a guard implied by Java's semantics, e.g. that an array index is in bounds.
+  // It should be possible to violate the condition the first time, but not the second,
+  // as the program would have aborted (without --java-throw-runtime-exceptions) or a
+  // runtime exception thrown (with --java-throw-runtime-exceptions).
+
+  public static void testAssertion(boolean condition) {
+    assert(condition);
+    assert(condition);
+  }
+
+  public static void testArrayBounds(int[] array, int index) {
+    if(array == null)
+      return;
+    int got = array[index];
+    got = array[index];
+  }
+
+  public static void testClassCast(boolean unknown) {
+    A maybe_b = unknown ? new A() : new B();
+    B definitely_b = (B)maybe_b;
+    definitely_b = (B)maybe_b;
+  }
+
+  public static void testNullDeref(A maybeNull) {
+    int got = maybeNull.field;
+    got = maybeNull.field;
+  }
+
+  public static void testDivByZero(int unknown) {
+    int div = 1 / unknown;
+    div = 1 / unknown;
+  }
+
+  public static void testArrayCreation(int maybeNegative) {
+    int[] arr = new int[maybeNegative];
+    arr = new int[maybeNegative];
+  }
+
+}
+
+class A { public int field; }
+class B extends A {}

regression/cbmc-java/repeated_guards/B.class

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.testArrayBounds
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+array-index-out-of-bounds-low\.1.*: FAILURE$
+array-index-out-of-bounds-low\.2.*: SUCCESS$
+array-index-out-of-bounds-high\.1.*: FAILURE$
+array-index-out-of-bounds-high\.2.*: SUCCESS$
+--
+^warning: ignoring

regression/cbmc-java/repeated_guards/Test.class

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testArrayCreation
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+array-create-negative-size\.1.*: FAILURE$
+array-create-negative-size\.2.*: SUCCESS$
+--
+^warning: ignoring

regression/cbmc-java/repeated_guards/Test.java

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testAssertion
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+assertion at file Test\.java line 10.*: FAILURE$
+assertion at file Test\.java line 11.*: SUCCESS$
+--
+^warning: ignoring

regression/cbmc-java/repeated_guards/test_arraybounds.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testClassCast
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+bad-dynamic-cast\.1.*: FAILURE$
+bad-dynamic-cast\.2.*: SUCCESS$
+--
+^warning: ignoring

regression/cbmc-java/repeated_guards/test_arraycreation.desc

@@ -0,0 +1,10 @@
+CORE
+Test.class
+--function Test.testDivByZero
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+integer-divide-by-zero\.1.*: FAILURE$
+integer-divide-by-zero\.2.*: SUCCESS$
+--
+^warning: ignoring