introduce code_havoc_objectt

This documents an existing codet variant.

Author: Daniel Kroening

Diff for: src/goto-programs/builtin_functions.cpp

@@ -809,9 +809,8 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
-    codet havoc(ID_havoc_object);
+    code_havoc_objectt havoc(arguments[0]);
     havoc.add_source_location() = function.source_location();
-    havoc.copy_to_operands(arguments[0]);
 
     dest.add(goto_programt::make_other(havoc, function.source_location()));
   }

Diff for: src/goto-symex/symex_other.cpp

@@ -256,11 +256,9 @@ void goto_symext::symex_other(
   }
   else if(statement==ID_havoc_object)
   {
-    DATA_INVARIANT(
-      code.operands().size() == 1,
-      "expected havoc_object statement to have one operand");
+    const auto &havoc_object_statement = to_code_havoc_object(code);
 
-    exprt object = clean_expr(code.op0(), state, false);
+    exprt object = clean_expr(havoc_object_statement.object(), state, false);
 
     process_array_expr(state, object);
     havoc_rec(state, guardt(true_exprt(), guard_manager), object);

Diff for: src/util/std_code.h

@@ -2380,6 +2380,59 @@ inline code_try_catcht &to_code_try_catch(codet &code)
   return ret;
 }
 
+/// \ref codet representation of a 'havoc_object' statement.
+class code_havoc_objectt : public codet
+{
+public:
+  explicit code_havoc_objectt(exprt op)
+    : codet(ID_havoc_object, {std::move(op)})
+  {
+  }
+
+  const exprt &object() const
+  {
+    return op0();
+  }
+
+  exprt &object()
+  {
+    return op0();
+  }
+
+protected:
+  using codet::op0;
+  using codet::op1;
+  using codet::op2;
+  using codet::op3;
+};
+
+template <>
+inline bool can_cast_expr<code_havoc_objectt>(const exprt &base)
+{
+  return detail::can_cast_code_impl(base, ID_havoc_object);
+}
+
+inline void validate_expr(const code_havoc_objectt &x)
+{
+  validate_operands(x, 1, "havoc_object must have one operand", true);
+}
+
+inline const code_havoc_objectt &to_code_havoc_object(const codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_havoc_object);
+  const code_havoc_objectt &ret = static_cast<const code_havoc_objectt &>(code);
+  validate_expr(ret);
+  return ret;
+}
+
+inline code_havoc_objectt &to_code_havoc_object(codet &code)
+{
+  PRECONDITION(code.get_statement() == ID_try_catch);
+  code_havoc_objectt &ret = static_cast<code_havoc_objectt &>(code);
+  validate_expr(ret);
+  return ret;
+}
+
 /// This class is used to interface between a language frontend
 /// and goto-convert -- it communicates the identifiers of the parameters
 /// of a function or method