From 24b488fa7fc7c651e8764d484313e8b126d80b91 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Thu, 6 Jun 2019 11:15:19 +0100
Subject: [PATCH] introduce code_havoc_objectt

This documents an existing codet variant.
---
 src/goto-programs/builtin_functions.cpp |  3 +-
 src/goto-symex/symex_other.cpp          |  6 +--
 src/util/std_code.h                     | 53 +++++++++++++++++++++++++
 3 files changed, 56 insertions(+), 6 deletions(-)

diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 1f00aaa2a23..bda11c19d82 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -793,9 +793,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 --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 2239878146d..0a92429c047 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/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 --git a/src/util/std_code.h b/src/util/std_code.h
index 4d7d1299c94..125190ce602 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -2473,6 +2473,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