check_class_cast: don't duplicate existing assertion

java_bytecode_convert_method.cpp already creates an assertion; we should
replace it with an appropriately elaborated one rather than leaving the
existing one in place.

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

@@ -327,7 +327,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)
@@ -338,13 +338,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)