Merge pull request #1098 from smowton/smowton/fix/cast_null_pointer

Accept null pointer casts

Author: smowton

regression/cbmc-java/cast_null1/test.class

@@ -0,0 +1,9 @@
+CORE
+test.class
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+Dynamic cast check: FAILURE
+^warning: ignoring

regression/cbmc-java/cast_null1/test.desc

@@ -0,0 +1,8 @@
+
+public class test {
+
+  public static void main() {
+    test t = (test)null;
+  }
+
+}

regression/cbmc-java/cast_null1/test.java

@@ -0,0 +1,8 @@
+CORE
+test.class
+--java-throw-runtime-exceptions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-java/cast_null2/test.class

@@ -0,0 +1,8 @@
+
+public class test {
+
+  public static void main() {
+    test t = (test)null;
+  }
+
+}

regression/cbmc-java/cast_null2/test.desc

@@ -200,26 +200,30 @@ codet java_bytecode_instrumentt::check_class_cast(
   exprt null_check_op=class1;
   if(null_check_op.type()!=voidptr)
     null_check_op.make_typecast(voidptr);
-  notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr));
-
-  // checkcast passes when the operand is null
-  and_exprt and_expr(op_not_null, not_exprt(class_cast_check));
 
+  codet check_code;
   if(throw_runtime_exceptions)
-    return throw_exception(
-      and_expr,
-      original_loc,
-      "ClassCastException");
-
-  code_assertt assert_class(class_cast_check);
-  assert_class.add_source_location().
-    set_comment("Dynamic cast check");
-  assert_class.add_source_location().
-    set_property_class("bad-dynamic-cast");
+  {
+    check_code=
+      throw_exception(
+        not_exprt(class_cast_check),
+        original_loc,
+        "ClassCastException");
+  }
+  else
+  {
+    code_assertt assert_class(class_cast_check);
+    assert_class.add_source_location().
+      set_comment("Dynamic cast check");
+    assert_class.add_source_location().
+      set_property_class("bad-dynamic-cast");
+    check_code=std::move(assert_class);
+  }
 
   code_ifthenelset conditional_check;
+  notequal_exprt op_not_null(null_check_op, null_pointer_exprt(voidptr));
   conditional_check.cond()=std::move(op_not_null);
-  conditional_check.then_case()=std::move(assert_class);
+  conditional_check.then_case()=std::move(check_code);
   return conditional_check;
 }
 
@@ -328,7 +332,7 @@ void java_bytecode_instrumentt::instrument_code(exprt &expr)
   }
   else if(statement==ID_assert)
   {
-    code_assertt code_assert=to_code_assert(code);
+    const code_assertt &code_assert=to_code_assert(code);
 
     // does this correspond to checkcast?
     if(code_assert.assertion().id()==ID_java_instanceof)
@@ -339,13 +343,11 @@ void java_bytecode_instrumentt::instrument_code(exprt &expr)
         code_assert.assertion().operands().size()==2,
         "Instanceof should have 2 operands");
 
-      block.copy_to_operands(
+      code=
         check_class_cast(
           code_assert.assertion().op0(),
           code_assert.assertion().op1(),
-          code_assert.source_location()));
-      block.copy_to_operands(code_assert);
-      code=block;
+          code_assert.source_location());
     }
   }
   else if(statement==ID_block)