Prepare for strict type checking in replace_symbolt

The derived class unchecked_replace_symbolt will not do any such type checking
and is to be used in all cases where types are expected to change or no type
checking can be performed.

Author: tautschnig

src/goto-instrument/model_argc_argv.cpp

@@ -130,7 +130,7 @@ bool model_argc_argv(
     {
       value = symbol_pair.second.value;
 
-      replace_symbolt replace;
+      unchecked_replace_symbolt replace;
       replace.insert(ARGC, ns.lookup("argc'").symbol_expr());
       replace.insert(ARGV, ns.lookup("argv'").symbol_expr());
       replace(value);

src/linking/linking_class.h

@@ -35,7 +35,7 @@ class linkingt:public typecheckt
   virtual void typecheck();
 
   rename_symbolt rename_symbol;
-  replace_symbolt object_type_updates;
+  unchecked_replace_symbolt object_type_updates;
 
 protected:
   bool needs_renaming_type(

src/util/replace_symbol.cpp

@@ -245,3 +245,10 @@ bool replace_symbolt::have_to_replace(const typet &dest) const
 
   return false;
 }
+
+void unchecked_replace_symbolt::insert(
+  const symbol_exprt &old_expr,
+  const exprt &new_expr)
+{
+  expr_map.emplace(old_expr.get_identifier(), new_expr);
+}

src/util/replace_symbol.h

@@ -97,4 +97,14 @@ class replace_symbolt
   bool have_to_replace(const typet &type) const;
 };
 
+class unchecked_replace_symbolt : public replace_symbolt
+{
+public:
+  unchecked_replace_symbolt()
+  {
+  }
+
+  void insert(const symbol_exprt &old_expr, const exprt &new_expr);
+};
+
 #endif // CPROVER_UTIL_REPLACE_SYMBOL_H