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/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"

src/goto-programs/remove_function_pointers.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <cassert>
 
-#include <util/base_type.h>
 #include <util/c_types.h>
 #include <util/fresh_symbol.h>
 #include <util/invariant.h>
@@ -22,7 +21,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/replace_expr.h>
 #include <util/source_location.h>
 #include <util/std_expr.h>
-#include <util/type_eq.h>
 
 #include <analyses/does_remove_const.h>
 
@@ -127,7 +125,7 @@ bool remove_function_pointerst::arg_is_type_compatible(
   const typet &call_type,
   const typet &function_type)
 {
-  if(type_eq(call_type, function_type, ns))
+  if(call_type == function_type)
     return true;
 
   // any integer-vs-enum-vs-pointer is ok
@@ -159,7 +157,7 @@ bool remove_function_pointerst::is_type_compatible(
   if(!return_value_used)
   {
   }
-  else if(type_eq(call_type.return_type(), empty_typet(), ns))
+  else if(call_type.return_type() == empty_typet())
   {
     // ok
   }
@@ -214,8 +212,7 @@ void remove_function_pointerst::fix_argument_types(
   {
     if(i<call_arguments.size())
     {
-      if(!type_eq(call_arguments[i].type(),
-                  function_parameters[i].type(), ns))
+      if(call_arguments[i].type() != function_parameters[i].type())
       {
         call_arguments[i].make_typecast(function_parameters[i].type());
       }
@@ -234,9 +231,7 @@ void remove_function_pointerst::fix_return_type(
   const code_typet &code_type = to_code_type(function_call.function().type());
 
   // type already ok?
-  if(type_eq(
-       function_call.lhs().type(),
-       code_type.return_type(), ns))
+  if(function_call.lhs().type() == code_type.return_type())
     return;
 
   const symbolt &function_symbol =

src/goto-programs/remove_virtual_functions.cpp

@@ -12,8 +12,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <algorithm>
 
-#include <util/type_eq.h>
-
 #include "class_identifier.h"
 #include "goto_model.h"
 #include "remove_skip.h"
@@ -130,7 +128,7 @@ static void create_static_function_call(
   {
     const typet &need_type = callee_parameters[i].type();
 
-    if(!type_eq(call_args[i].type(), need_type, ns))
+    if(call_args[i].type() != need_type)
     {
       // If this wasn't language agnostic code we'd also like to check
       // compatibility-- for example, Java overrides may have differing generic

src/goto-programs/replace_calls.cpp

@@ -15,7 +15,6 @@ Author: Daniel Poetzl
 
 #include <goto-programs/remove_returns.h>
 
-#include <util/base_type.h>
 #include <util/exception_utils.h>
 #include <util/invariant.h>
 #include <util/irep.h>
@@ -94,7 +93,7 @@ void replace_callst::operator()(
     auto f_it2 = goto_functions.function_map.find(new_id);
     PRECONDITION(f_it2 != goto_functions.function_map.end());
 
-    PRECONDITION(base_type_eq(f_it1->second.type, f_it2->second.type, ns));
+    PRECONDITION(f_it1->second.type == f_it2->second.type);
 
     // check that returns have not been removed
     goto_programt::const_targett next_it = std::next(it);
@@ -165,7 +164,7 @@ void replace_callst::check_replacement_map(
     auto it1 = goto_functions.function_map.find(p.first);
     if(it1 != goto_functions.function_map.end())
     {
-      if(!base_type_eq(it1->second.type, it2->second.type, ns))
+      if(it1->second.type != it2->second.type)
         throw invalid_command_line_argument_exceptiont(
           "functions " + id2string(p.first) + " and " + id2string(p.second) +
             " are not type-compatible",