Use conditional_cast instead of make_type

No need for a local helper that unnecessarily used `follow`.

src/goto-programs/printf_formatter.cpp

@@ -16,17 +16,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/format_constant.h>
 #include <util/pointer_expr.h>
-#include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
-const exprt printf_formattert::make_type(
-  const exprt &src, const typet &dest)
-{
-  if(src.type()==dest)
-    return src;
-  return simplify_expr(typecast_exprt(src, dest), ns);
-}
-
 void printf_formattert::operator()(
   const std::string &_format,
   const std::list<exprt> &_operands)
@@ -106,7 +97,7 @@ void printf_formattert::process_format(std::ostream &out)
     if(next_operand==operands.end())
       break;
     out << format_constant(
-      make_type(*(next_operand++), double_type()));
+      typecast_exprt::conditional_cast(*(next_operand++), double_type()));
     break;
 
   case 'f':
@@ -115,7 +106,7 @@ void printf_formattert::process_format(std::ostream &out)
     if(next_operand==operands.end())
       break;
     out << format_constant(
-      make_type(*(next_operand++), double_type()));
+      typecast_exprt::conditional_cast(*(next_operand++), double_type()));
     break;
 
   case 'g':
@@ -126,7 +117,7 @@ void printf_formattert::process_format(std::ostream &out)
     if(next_operand==operands.end())
       break;
     out << format_constant(
-      make_type(*(next_operand++), double_type()));
+      typecast_exprt::conditional_cast(*(next_operand++), double_type()));
     break;
 
   case 's':
@@ -151,28 +142,28 @@ void printf_formattert::process_format(std::ostream &out)
     if(next_operand==operands.end())
       break;
     out << format_constant(
-      make_type(*(next_operand++), signed_int_type()));
+      typecast_exprt::conditional_cast(*(next_operand++), signed_int_type()));
     break;
 
   case 'D':
     if(next_operand==operands.end())
       break;
-    out << format_constant(
-      make_type(*(next_operand++), signed_long_int_type()));
+    out << format_constant(typecast_exprt::conditional_cast(
+      *(next_operand++), signed_long_int_type()));
     break;
 
   case 'u':
     if(next_operand==operands.end())
       break;
     out << format_constant(
-      make_type(*(next_operand++), unsigned_int_type()));
+      typecast_exprt::conditional_cast(*(next_operand++), unsigned_int_type()));
     break;
 
   case 'U':
     if(next_operand==operands.end())
       break;
-    out << format_constant(
-      make_type(*(next_operand++), unsigned_long_int_type()));
+    out << format_constant(typecast_exprt::conditional_cast(
+      *(next_operand++), unsigned_long_int_type()));
     break;
 
   default:

src/goto-programs/printf_formatter.h

@@ -51,8 +51,6 @@ class printf_formattert
 
   void process_char(std::ostream &out);
   void process_format(std::ostream &out);
-
-  const exprt make_type(const exprt &src, const typet &dest);
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_PRINTF_FORMATTER_H

src/goto-programs/string_abstraction.cpp

@@ -442,10 +442,9 @@ symbol_exprt string_abstractiont::add_dummy_symbol_and_value(
        build_unknown(whatt::LENGTH, false),
        to_array_type(source_type).size().id() == ID_infinity
          ? build_unknown(whatt::SIZE, false)
-         : to_array_type(source_type).size()},
+         : typecast_exprt::conditional_cast(
+             to_array_type(source_type).size(), build_type(whatt::SIZE))},
       string_struct);
-
-    make_type(to_struct_expr(new_symbol.value).op2(), build_type(whatt::SIZE));
   }
   else
     new_symbol.value=
@@ -1212,8 +1211,8 @@ goto_programt::targett string_abstractiont::abstract_char_assign(
         i2.is_not_nil(),
         "failed to create length-component for the left-hand-side");
 
-      exprt new_length=i_lhs.index();
-      make_type(new_length, i2.type());
+      exprt new_length =
+        typecast_exprt::conditional_cast(i_lhs.index(), i2.type());
 
       if_exprt min_expr(binary_relation_exprt(new_length, ID_lt, i2),
           new_length, i2);
@@ -1232,16 +1231,14 @@ goto_programt::targett string_abstractiont::abstract_char_assign(
         i2.is_not_nil(),
         "failed to create length-component for the left-hand-side");
 
-      make_type(ptr.offset, build_type(whatt::LENGTH));
-      return
-        char_assign(
-          dest,
-          target,
-          new_lhs,
-          i2,
-          ptr.offset.is_nil()?
-            from_integer(0, build_type(whatt::LENGTH)):
-            ptr.offset);
+      return char_assign(
+        dest,
+        target,
+        new_lhs,
+        i2,
+        ptr.offset.is_nil() ? from_integer(0, build_type(whatt::LENGTH))
+                            : typecast_exprt::conditional_cast(
+                                ptr.offset, build_type(whatt::LENGTH)));
     }
   }
 

src/goto-programs/string_abstraction.h

@@ -73,13 +73,6 @@ class string_abstractiont
 
   bool is_ptr_string_struct(const typet &type) const;
 
-  void make_type(exprt &dest, const typet &type)
-  {
-    if(dest.is_not_nil() &&
-       ns.follow(dest.type())!=ns.follow(type))
-      dest = typecast_exprt(dest, type);
-  }
-
   goto_programt::targett abstract(
     goto_programt &dest, goto_programt::targett it);
   goto_programt::targett abstract_assign(

src/goto-programs/string_instrumentation.cpp

@@ -64,12 +64,6 @@ class string_instrumentationt
   symbol_table_baset &symbol_table;
   namespacet ns;
 
-  void make_type(exprt &dest, const typet &type)
-  {
-    if(ns.follow(dest.type())!=ns.follow(type))
-      dest = typecast_exprt(dest, type);
-  }
-
   void instrument(goto_programt &dest, goto_programt::targett it);
   void do_function_call(goto_programt &dest, goto_programt::targett target);
 
@@ -785,8 +779,7 @@ void string_instrumentationt::do_strerror(
 
   // assign address
   {
-    exprt rhs=ptr;
-    make_type(rhs, lhs.type());
+    exprt rhs = typecast_exprt::conditional_cast(ptr, lhs.type());
     tmp.add(goto_programt::make_assignment(
       code_assignt(lhs, rhs), it->source_location()));
   }