use typecast_exprt::conditional_cast

.make_typecast() isn't type save; when used in the pattern
if(a.type()!=b.type()) ... then use typecast_exprt::conditional_cast
instead.

Author: Daniel Kroening

src/analyses/escape_analysis.cpp

@@ -421,8 +421,9 @@ void escape_analysist::insert_cleanup(
       exprt arg=lhs;
       if(is_object)
         arg=address_of_exprt(arg);
-      if(arg.type()!=param_type)
-        arg.make_typecast(param_type);
+
+      arg = typecast_exprt::conditional_cast(arg, param_type);
+
       code.arguments().push_back(arg);
     }
 

src/analyses/goto_check.cpp

@@ -1293,18 +1293,19 @@ void goto_checkt::bounds_check(
     const exprt &pointer=
       to_dereference_expr(ode.root_object()).pointer();
 
-    if_exprt size(
+    const if_exprt size(
       dynamic_object(pointer),
       typecast_exprt(dynamic_size(ns), object_size(pointer).type()),
       object_size(pointer));
 
-    plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
+    const plus_exprt effective_offset(ode.offset(), pointer_offset(pointer));
 
     assert(effective_offset.op0().type()==effective_offset.op1().type());
-    if(effective_offset.type()!=size.type())
-      size.make_typecast(effective_offset.type());
 
-    binary_relation_exprt inequality(effective_offset, ID_lt, size);
+    const auto size_casted =
+      typecast_exprt::conditional_cast(size, effective_offset.type());
+
+    binary_relation_exprt inequality(effective_offset, ID_lt, size_casted);
 
     or_exprt precond(
       and_exprt(

src/solvers/flattening/arrays.cpp

@@ -325,12 +325,8 @@ void arrayst::add_array_Ackermann_constraints()
           // index equality
           equal_exprt indices_equal(*i1, *i2);
 
-          if(indices_equal.op0().type()!=
-             indices_equal.op1().type())
-          {
-            indices_equal.op1().
-              make_typecast(indices_equal.op0().type());
-          }
+          indices_equal.op1() = typecast_exprt::conditional_cast(
+            indices_equal.op1(), indices_equal.op0().type());
 
           literalt indices_equal_lit=convert(indices_equal);
 
@@ -537,8 +533,7 @@ void arrayst::add_array_constraints_with(
     {
       // we first build the guard
 
-      if(other_index.type()!=index.type())
-        other_index.make_typecast(index.type());
+      other_index = typecast_exprt::conditional_cast(other_index, index.type());
 
       literalt guard_lit=convert(equal_exprt(index, other_index));
 

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -91,8 +91,10 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
     object_descriptor_exprt o;
     o.build(expr.op(), ns);
     CHECK_RETURN(o.offset().id() != ID_unknown);
-    if(o.offset().type() != expr.offset().type())
-      o.offset().make_typecast(expr.offset().type());
+
+    o.offset() =
+      typecast_exprt::conditional_cast(o.offset(), expr.offset().type());
+
     byte_extract_exprt be(
       expr.id(),
       o.root_object(),

src/solvers/lowering/byte_operators.cpp

@@ -396,9 +396,7 @@ static exprt lower_byte_update(
 
           if(i==0 && element_size==1) // bytes?
           {
-            new_value = src.value();
-            if(new_value.type()!=subtype)
-              new_value.make_typecast(subtype);
+            new_value = typecast_exprt::conditional_cast(src.value(), subtype);
           }
           else
           {

src/util/pointer_offset_size.cpp

@@ -311,15 +311,14 @@ exprt size_of_expr(
       return nil_exprt();
 
     // get size
-    exprt size = array_type.size();
+    const auto size = array_type.size();
 
     if(size.is_nil())
       return nil_exprt();
 
-    if(size.type()!=sub.type())
-      size.make_typecast(sub.type());
+    const auto size_casted = typecast_exprt::conditional_cast(size, sub.type());
 
-    mult_exprt result(size, sub);
+    mult_exprt result(size_casted, sub);
     simplify(result, ns);
 
     return std::move(result);
@@ -342,15 +341,14 @@ exprt size_of_expr(
       return nil_exprt();
 
     // get size
-    exprt size=to_vector_type(type).size();
+    const auto size = to_vector_type(type).size();
 
     if(size.is_nil())
       return nil_exprt();
 
-    if(size.type()!=sub.type())
-      size.make_typecast(sub.type());
+    const auto size_casted = typecast_exprt::conditional_cast(size, sub.type());
 
-    mult_exprt result(size, sub);
+    mult_exprt result(size_casted, sub);
     simplify(result, ns);
 
     return std::move(result);
@@ -633,10 +631,7 @@ exprt build_sizeof_expr(
   if(remainder>0)
     result=plus_exprt(result, from_integer(remainder, t));
 
-  if(result.type()!=expr.type())
-    result.make_typecast(expr.type());
-
-  return result;
+  return typecast_exprt::conditional_cast(result, expr.type());
 }
 
 exprt get_subexpression_at_offset(

src/util/pointer_predicates.cpp

@@ -171,17 +171,16 @@ exprt dynamic_object_upper_bound(
   {
     op=ID_gt;
 
-    if(ns.follow(object_offset.type())!=
-       ns.follow(access_size.type()))
-      object_offset.make_typecast(access_size.type());
-    sum=plus_exprt(object_offset, access_size);
+    const auto object_offset_casted =
+      typecast_exprt::conditional_cast(object_offset, access_size.type());
+
+    sum = plus_exprt(object_offset_casted, access_size);
   }
 
-  if(ns.follow(sum.type())!=
-     ns.follow(malloc_size.type()))
-    sum.make_typecast(malloc_size.type());
+  const auto sum_casted =
+    typecast_exprt::conditional_cast(sum, malloc_size.type());
 
-  return binary_relation_exprt(sum, op, malloc_size);
+  return binary_relation_exprt(sum_casted, op, malloc_size);
 }
 
 exprt object_upper_bound(
@@ -204,16 +203,14 @@ exprt object_upper_bound(
   {
     op=ID_gt;
 
-    if(ns.follow(object_offset.type())!=
-       ns.follow(access_size.type()))
-      object_offset.make_typecast(access_size.type());
+    const auto object_offset_casted =
+      typecast_exprt::conditional_cast(object_offset, access_size.type());
+
     sum=plus_exprt(object_offset, access_size);
   }
 
-
-  if(ns.follow(sum.type())!=
-     ns.follow(object_size_expr.type()))
-    sum.make_typecast(object_size_expr.type());
+  const auto sum_casted =
+    typecast_exprt::conditional_cast(sum, object_size_expr.type());
 
   return binary_relation_exprt(sum, op, object_size_expr);
 }

src/util/simplify_expr_array.cpp

@@ -81,10 +81,10 @@ bool simplify_exprt::simplify_index(exprt &expr)
     {
       // Turn (a with i:=x)[j] into (i==j)?x:a[j].
       // watch out that the type of i and j might be different.
-      equal_exprt equality_expr(expr.op1(), with_expr.op1());
+      const exprt rhs_casted =
+        typecast_exprt::conditional_cast(with_expr.op1(), expr.op1().type());
 
-      if(equality_expr.lhs().type()!=equality_expr.rhs().type())
-        equality_expr.rhs().make_typecast(equality_expr.lhs().type());
+      equal_exprt equality_expr(expr.op1(), rhs_casted);
 
       simplify_inequality(equality_expr);
 

src/util/simplify_expr_pointer.cpp

@@ -287,21 +287,15 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
              tmp.op0().operands().size()==1 &&
              tmp.op0().op0().id()==ID_address_of)
           {
-            expr=tmp.op1();
-            if(type!=expr.type())
-              expr.make_typecast(type);
-
+            expr = typecast_exprt::conditional_cast(tmp.op1(), type);
             simplify_node(expr);
             return false;
           }
           else if(tmp.op1().id()==ID_typecast &&
                   tmp.op1().operands().size()==1 &&
                   tmp.op1().op0().id()==ID_address_of)
           {
-            expr=tmp.op0();
-            if(type!=expr.type())
-              expr.make_typecast(type);
-
+            expr = typecast_exprt::conditional_cast(tmp.op0(), type);
             simplify_node(expr);
             return false;
           }