remove base_type_eq and type_eq

These are no longer needed, as symbol_type is no longer in use.

Author: Daniel Kroening

jbmc/unit/java-testing-utils/require_type.cpp

@@ -9,7 +9,6 @@ Author: Diffblue Ltd.
 #include "require_type.h"
 
 #include <testing-utils/use_catch.h>
-#include <util/base_type.h>
 #include <util/namespace.h>
 #include <util/symbol_table.h>
 
@@ -26,10 +25,8 @@ pointer_typet require_type::require_pointer(
   const pointer_typet &pointer = to_pointer_type(type);
 
   if(subtype)
-  {
-    namespacet ns{symbol_tablet{}};
-    base_type_eq(pointer.subtype(), subtype.value(), ns);
-  }
+    REQUIRE(pointer.subtype() == subtype.value());
+
   return pointer;
 }
 

src/analyses/constant_propagator.cpp

@@ -17,7 +17,6 @@ Author: Peter Schrammel
 #endif
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
@@ -103,7 +102,7 @@ void constant_propagator_domaint::assign_rec(
     if(dest_values.is_constant(tmp))
     {
       DATA_INVARIANT(
-        base_type_eq(ns.lookup(s).type, tmp.type(), ns),
+        ns.lookup(s).type == tmp.type(),
         "type of constant to be replaced should match");
       dest_values.set_to(s, tmp);
     }
@@ -623,7 +622,7 @@ bool constant_propagator_domaint::valuest::meet(
     {
       const typet &m_id_type = ns.lookup(m.first).type;
       DATA_INVARIANT(
-        base_type_eq(m_id_type, m.second.type(), ns),
+        m_id_type == m.second.type(),
         "type of constant to be stored should match");
       set_to(symbol_exprt(m.first, m_id_type), m.second);
       changed=true;

src/analyses/does_remove_const.cpp

@@ -15,7 +15,6 @@ Author: Diffblue Ltd.
 #include <util/type.h>
 #include <util/expr.h>
 #include <util/std_code.h>
-#include <util/base_type.h>
 
 /// A naive analysis to look for casts that remove const-ness from pointers.
 /// \param goto_program: the goto program to check
@@ -74,7 +73,7 @@ bool does_remove_constt::does_expr_lose_const(const exprt &expr) const
   for(const exprt &op : expr.operands())
   {
     const typet &op_type=op.type();
-    if(base_type_eq(op_type, root_type, ns))
+    if(op_type == root_type)
     {
       // Is this child more const-qualified than the root
       if(!does_type_preserve_const_correctness(&root_type, &op_type))

src/analyses/goto_check.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/array_name.h>
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>

src/analyses/invariant_propagation.cpp

@@ -12,7 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include "invariant_propagation.h"
 
 #include <util/simplify_expr.h>
-#include <util/base_type.h>
 #include <util/symbol_table.h>
 #include <util/std_expr.h>
 

src/analyses/invariant_set.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/base_exceptions.h>
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/expr_util.h>
 #include <util/namespace.h>

src/analyses/local_safe_pointers.cpp

@@ -11,7 +11,6 @@ Author: Diffblue Ltd
 
 #include "local_safe_pointers.h"
 
-#include <util/base_type.h>
 #include <util/expr_iterator.h>
 #include <util/expr_util.h>
 #include <util/format_expr.h>
@@ -275,7 +274,7 @@ bool local_safe_pointerst::is_non_null_at_program_point(
 bool local_safe_pointerst::base_type_comparet::operator()(
   const exprt &e1, const exprt &e2) const
 {
-  if(base_type_eq(e1, e2, ns))
+  if(e1 == e2)
     return false;
   else
     return e1 < e2;

src/ansi-c/c_typecast.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_util.h>
@@ -551,7 +550,7 @@ void c_typecastt::implicit_typecast_followed(
         // very generous:
         // between any two function pointers it's ok
       }
-      else if(base_type_eq(src_sub, dest_sub, ns))
+      else if(src_sub == dest_sub)
       {
         // ok
       }
@@ -565,9 +564,9 @@ void c_typecastt::implicit_typecast_followed(
         // Also generous: between any to scalar types it's ok.
         // We should probably check the size.
       }
-      else if(src_sub.id()==ID_array &&
-              dest_sub.id()==ID_array &&
-              base_type_eq(src_sub.subtype(), dest_sub.subtype(), ns))
+      else if(
+        src_sub.id() == ID_array && dest_sub.id() == ID_array &&
+        src_sub.subtype() == dest_sub.subtype())
       {
         // we ignore the size of the top-level array
         // in the case of pointers to arrays

src/ansi-c/c_typecheck_expr.cpp

@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
@@ -1064,9 +1063,9 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
 
   const typet expr_type=follow(expr.type());
 
-  if(expr_type.id()==ID_union &&
-     !base_type_eq(expr_type, op.type(), *this) &&
-     op.id()!=ID_initializer_list)
+  if(
+    expr_type.id() == ID_union && expr_type != op.type() &&
+    op.id() != ID_initializer_list)
   {
     // This is a GCC extension. It's either a 'temporary union',
     // where the argument is one of the member types.
@@ -1080,7 +1079,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
     // we need to find a member with the right type
     for(const auto &c : to_union_type(expr_type).components())
     {
-      if(base_type_eq(c.type(), op.type(), *this))
+      if(c.type() == op.type())
       {
         // found! build union constructor
         union_exprt union_expr(c.get_name(), op, expr.type());
@@ -1131,7 +1130,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
   const typet op_type = op.type();
 
   // cast to same type?
-  if(base_type_eq(expr_type, op_type, *this))
+  if(expr_type == op_type)
     return; // it's ok
 
   // vectors?
@@ -2516,8 +2515,7 @@ exprt c_typecheck_baset::do_special_functions(
       expr.arguments().front(), expr.arguments().back());
     equality_expr.add_source_location()=source_location;
 
-    if(!base_type_eq(equality_expr.lhs().type(),
-                     equality_expr.rhs().type(), *this))
+    if(equality_expr.lhs().type() != equality_expr.rhs().type())
     {
       error().source_location = f_op.source_location();
       error() << "equal expects two operands of same type" << eom;

src/ansi-c/c_typecheck_initializer.cpp

@@ -19,7 +19,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/std_types.h>
 #include <util/string_constant.h>
-#include <util/type_eq.h>
 
 #include "anonymous_member.h"
 

src/cpp/cpp_typecheck_expr.cpp

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
 #endif
 
 #include <util/arith_tools.h>
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_initializer.h>
@@ -2373,9 +2372,9 @@ void cpp_typecheckt::typecheck_method_application(
     if(expr.arguments().size()==func_type.parameters().size())
     {
       // this might be set up for base-class initialisation
-      if(!base_type_eq(expr.arguments().front().type(),
-                      func_type.parameters().front().type(),
-                      *this))
+      if(
+        expr.arguments().front().type() !=
+        func_type.parameters().front().type())
       {
         implicit_typecast(expr.arguments().front(), this_type);
         assert(is_reference(expr.arguments().front().type()));

src/goto-instrument/dump_c.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "dump_c.h"
 
-#include <util/base_type.h>
 #include <util/config.h>
 #include <util/find_symbols.h>
 #include <util/invariant.h>
@@ -1277,9 +1276,9 @@ void dump_ct::cleanup_expr(exprt &expr)
       expr.swap(tmp);
     }
   }
-  else if(expr.id()==ID_typecast &&
-      expr.op0().id()==ID_typecast &&
-      base_type_eq(expr.type(), expr.op0().type(), ns))
+  else if(
+    expr.id() == ID_typecast && expr.op0().id() == ID_typecast &&
+    expr.type() == expr.op0().type())
   {
     exprt tmp=expr.op0();
     expr.swap(tmp);
@@ -1309,8 +1308,7 @@ void dump_ct::cleanup_expr(exprt &expr)
           if(type.id()==ID_union &&
              type.get_bool(ID_C_transparent_union))
           {
-            if(it2->id()==ID_typecast &&
-               base_type_eq(it2->type(), type, ns))
+            if(it2->id() == ID_typecast && it2->type() == type)
               *it2=to_typecast_expr(*it2).op();
 
             // add a typecast for NULL or 0

src/goto-instrument/goto_program2code.cpp

@@ -20,7 +20,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/find_symbols.h>
 #include <util/prefix.h>
 #include <util/simplify_expr.h>
-#include <util/type_eq.h>
 
 void goto_program2codet::operator()()
 {
@@ -1875,7 +1874,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
         if(!has_prefix(id2string(it->second.base_name), "nondet_"))
           continue;
         const code_typet &code_type=to_code_type(it->second.type);
-        if(!type_eq(code_type.return_type(), expr.type(), ns))
+        if(code_type.return_type() != expr.type())
           continue;
         if(!code_type.parameters().empty())
           continue;

src/goto-programs/goto_convert_functions.cpp

@@ -10,7 +10,6 @@ Date: June 2003
 
 #include "goto_convert_functions.h"
 
-#include <util/base_type.h>
 #include <util/fresh_symbol.h>
 #include <util/prefix.h>
 #include <util/std_code.h>

src/goto-programs/goto_inline.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/prefix.h>
 #include <util/cprover_prefix.h>
-#include <util/base_type.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 

src/goto-programs/goto_inline_class.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #endif
 
-#include <util/base_type.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_util.h>
 #include <util/invariant.h>
@@ -91,7 +90,7 @@ void goto_inlinet::parameter_assignments(
     {
       // it should be the same exact type as the parameter,
       // subject to some exceptions
-      if(!base_type_eq(par_type, actual.type(), ns))
+      if(par_type != actual.type())
       {
         const typet &f_partype = par_type;
         const typet &f_acttype = actual.type();

src/goto-programs/goto_program.cpp

@@ -713,7 +713,7 @@ void goto_programt::instructiont::validate(
         if(!ns.lookup(goto_id, table_symbol))
         {
           bool symbol_expr_type_matches_symbol_table =
-            base_type_eq(goto_symbol_expr.type(), table_symbol->type, ns);
+            goto_symbol_expr.type() == table_symbol->type;
 
           if(
             !symbol_expr_type_matches_symbol_table &&
@@ -722,10 +722,9 @@ void goto_programt::instructiont::validate(
             // Return removal sets the return type of a function symbol table
             // entry to 'void', but some callsites still expect the original
             // type (e.g. if a function is passed as a parameter)
-            symbol_expr_type_matches_symbol_table = base_type_eq(
-              goto_symbol_expr.type(),
-              original_return_type(ns.get_symbol_table(), goto_id),
-              ns);
+            symbol_expr_type_matches_symbol_table =
+              goto_symbol_expr.type() ==
+              original_return_type(ns.get_symbol_table(), goto_id);
 
             if(
               !symbol_expr_type_matches_symbol_table &&
@@ -749,7 +748,7 @@ void goto_programt::instructiont::validate(
                   table_symbol_type.return_type();
 
                 symbol_expr_type_matches_symbol_table =
-                  base_type_eq(goto_symbol_expr_type, table_symbol_type, ns);
+                  goto_symbol_expr_type == table_symbol_type;
               }
             }
           }
@@ -767,8 +766,8 @@ void goto_programt::instructiont::validate(
               auto symbol_table_array_type = to_array_type(table_symbol->type);
               symbol_table_array_type.size() = nil_exprt();
 
-              symbol_expr_type_matches_symbol_table = base_type_eq(
-                goto_symbol_expr.type(), symbol_table_array_type, ns);
+              symbol_expr_type_matches_symbol_table =
+                goto_symbol_expr.type() == symbol_table_array_type;
             }
           }
 

src/goto-programs/graphml_witness.cpp

@@ -11,7 +11,6 @@ Author: Daniel Kroening
 
 #include "graphml_witness.h"
 
-#include <util/base_type.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/arith_tools.h>
@@ -75,8 +74,9 @@ std::string graphml_witnesst::convert_assign_rec(
   {
     // dereferencing may have resulted in an lhs that is the first
     // struct member; undo this
-    if(assign.lhs().id()==ID_member &&
-       !base_type_eq(assign.lhs().type(), assign.rhs().type(), ns))
+    if(
+      assign.lhs().id() == ID_member &&
+      assign.lhs().type() != assign.rhs().type())
     {
       code_assignt tmp=assign;
       tmp.lhs()=to_member_expr(assign.lhs()).struct_op();

src/goto-programs/link_goto_model.cpp

@@ -13,7 +13,6 @@ Author: Michael Tautschnig, Daniel Kroening
 
 #include <unordered_set>
 
-#include <util/base_type.h>
 #include <util/symbol.h>
 #include <util/rename_symbol.h>
 
@@ -102,8 +101,9 @@ static bool link_functions(
       {
         // the linking code will have ensured that types match
         rename_symbol(src_func.type);
-        INVARIANT(base_type_eq(in_dest_symbol_table.type, src_func.type, ns),
-                  "linking ensures that types match");
+        INVARIANT(
+          in_dest_symbol_table.type == src_func.type,
+          "linking ensures that types match");
       }
     }
   }

src/goto-programs/read_goto_binary.cpp

@@ -18,7 +18,6 @@ Module: Read Goto Programs
 #include <util/unicode.h>
 #include <util/tempfile.h>
 #include <util/rename_symbol.h>
-#include <util/base_type.h>
 #include <util/config.h>
 
 #include "goto_model.h"