replace_expr: check type consistency

Make sure that replace_expr cannot introduce type-inconsistent
expressions. This wouldn't be a fault of replace_expr, but rather
requires fixing the caller. Add preconditions to check this.

Author: tautschnig

src/util/replace_expr.cpp

@@ -11,6 +11,11 @@ Author: Daniel Kroening, [email protected]
 
 bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
 {
+  PRECONDITION_WITH_DIAGNOSTICS(
+    what.type() == by.type(),
+    "types to be replaced should match. old type:\n" + what.type().pretty() +
+      "\nnew type:\n" + by.type().pretty());
+
   bool no_change = true;
 
   for(auto it = dest.depth_begin(), itend = dest.depth_end();
@@ -39,6 +44,11 @@ bool replace_expr(const replace_mapt &what, exprt &dest)
     replace_mapt::const_iterator findit = what.find(*it);
     if(findit != what.end())
     {
+      PRECONDITION_WITH_DIAGNOSTICS(
+        it->type() == findit->second.type(),
+        "types to be replaced should match. old type:\n" + it->type().pretty() +
+          "\nnew type:\n" + findit->second.type().pretty());
+
       it.mutate() = findit->second;
       no_change = false;
       it.next_sibling_or_parent();