equal_exprt now checks types of the operands

This commit adds a precondition to the constructor of equal_exprt, which
enforces that the two operands have the same type.

Author: kroening

src/cpp/cpp_typecheck_code.cpp

@@ -73,7 +73,8 @@ void cpp_typecheckt::typecheck_code(codet &code)
           shl_exprt shl{from_integer(1, array.type()),
                         to_index_expr(binary_expr.op0()).index()};
           exprt rhs = if_exprt{
-            equal_exprt{binary_expr.op1(), from_integer(0, array.type())},
+            equal_exprt{
+              binary_expr.op1(), from_integer(0, binary_expr.op1().type())},
             bitand_exprt{array, bitnot_exprt{shl}},
             bitor_exprt{array, shl}};
           binary_expr.op0() = to_index_expr(binary_expr.op0()).array();

src/goto-symex/symex_other.cpp

@@ -224,11 +224,13 @@ void goto_symext::symex_other(
     process_array_expr(state, array1);
     process_array_expr(state, array2);
 
-    exprt rhs = equal_exprt(array1, array2);
+    exprt rhs;
 
-    // check for size (or type) mismatch
+    // Types don't match? Make it 'false'.
     if(array1.type() != array2.type())
       rhs = false_exprt();
+    else
+      rhs = equal_exprt(array1, array2);
 
     symex_assign(state, code.op2(), rhs);
   }

src/linking/linking.cpp

@@ -949,6 +949,17 @@ bool linkingt::adjust_object_type_rec(
     }
     else
     {
+      if(new_size.type() != old_size.type())
+      {
+        link_error(
+          info.old_symbol,
+          info.new_symbol,
+          "conflicting array sizes for variable");
+
+        // error logged, continue typechecking other symbols
+        return true;
+      }
+
       equal_exprt eq(old_size, new_size);
 
       if(!simplify_expr(eq, ns).is_true())

src/util/std_expr.h

@@ -1308,6 +1308,7 @@ class equal_exprt:public binary_relation_exprt
   equal_exprt(exprt _lhs, exprt _rhs)
     : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
   {
+    PRECONDITION(lhs().type() == rhs().type());
   }
 
   static void check(

unit/goto-symex/try_evaluate_pointer_comparisons.cpp

@@ -80,16 +80,14 @@ SCENARIO(
       }
     }
 
-    WHEN("Evaluating ptr1 == (long*)(short*)&value1")
+    WHEN("Evaluating ptr1 == (int*)(short*)&value1")
     {
       const signedbv_typet long_type{64};
       const signedbv_typet short_type{16};
-      const pointer_typet ptr_long_type = pointer_type(long_type);
       const pointer_typet ptr_short_type = pointer_type(short_type);
       const equal_exprt comparison{
         ptr1,
-        typecast_exprt{typecast_exprt{address1, ptr_short_type},
-                       ptr_long_type}};
+        typecast_exprt{typecast_exprt{address1, ptr_short_type}, ptr_type}};
       const renamedt<exprt, L2> renamed_comparison =
         state.rename(comparison, ns);
       auto result = try_evaluate_pointer_comparisons(