diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt index 656ec83e465..9c26f7f84db 100644 --- a/scripts/expected_doxygen_warnings.txt +++ b/scripts/expected_doxygen_warnings.txt @@ -92,10 +92,10 @@ warning: Included by graph for 'expr_util.h' not generated, too many nodes (60), warning: Included by graph for 'invariant.h' not generated, too many nodes (187), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'irep.h' not generated, too many nodes (62), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'message.h' not generated, too many nodes (116), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'namespace.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'namespace.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (76), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'std_expr.h' not generated, too many nodes (246), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'std_types.h' not generated, too many nodes (124), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'std_types.h' not generated, too many nodes (123), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. diff --git a/src/analyses/does_remove_const.cpp b/src/analyses/does_remove_const.cpp index 265cdda8936..443c3e52c57 100644 --- a/src/analyses/does_remove_const.cpp +++ b/src/analyses/does_remove_const.cpp @@ -15,7 +15,6 @@ Author: Diffblue Ltd. #include #include #include -#include /// 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)) diff --git a/src/goto-instrument/replace_calls.cpp b/src/goto-instrument/replace_calls.cpp index fe28bea210f..7c1a2735d5c 100644 --- a/src/goto-instrument/replace_calls.cpp +++ b/src/goto-instrument/replace_calls.cpp @@ -15,7 +15,6 @@ Author: Daniel Poetzl #include -#include #include #include #include @@ -165,12 +164,13 @@ 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( - ns.lookup(it1->first).type, ns.lookup(it2->first).type, ns)) + if(ns.lookup(it1->first).type != ns.lookup(it2->first).type) + { throw invalid_command_line_argument_exceptiont( "functions " + id2string(p.first) + " and " + id2string(p.second) + " are not type-compatible", "--replace-calls"); + } } } } diff --git a/src/goto-instrument/value_set_fi_fp_removal.cpp b/src/goto-instrument/value_set_fi_fp_removal.cpp index 5dfce774ee0..e3c058b75f7 100644 --- a/src/goto-instrument/value_set_fi_fp_removal.cpp +++ b/src/goto-instrument/value_set_fi_fp_removal.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include #include diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp index 56955528cc2..98e03dfa216 100644 --- a/src/goto-programs/goto_program.cpp +++ b/src/goto-programs/goto_program.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -740,7 +739,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 && @@ -763,7 +762,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; } } diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp index 22c62f20c7e..a94784be641 100644 --- a/src/goto-programs/link_goto_model.cpp +++ b/src/goto-programs/link_goto_model.cpp @@ -13,7 +13,6 @@ Author: Michael Tautschnig, Daniel Kroening #include -#include #include #include @@ -123,15 +122,14 @@ static bool link_functions( INVARIANT(symbol.value.id() == ID_symbol, "must have symbol"); const irep_idt &id = to_symbol_expr(symbol.value).get_identifier(); - #if 0 - if(!base_type_eq(symbol.type, ns.lookup(id).type, ns)) +#if 0 + if(symbol.type != ns.lookup(id).type) { std::cerr << symbol << '\n'; std::cerr << ns.lookup(id) << '\n'; } - INVARIANT(base_type_eq(symbol.type, ns.lookup(id).type, ns), - "type matches"); - #endif + INVARIANT(symbol.type == ns.lookup(id).type, "type matches"); +#endif macro_application.insert_expr(symbol.name, id); } diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 880ca9d8861..a24237a44c7 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include @@ -139,8 +138,7 @@ void linkingt::detailed_conflict_report_rec( else if(t1.id()==ID_pointer || t1.id()==ID_array) { - if(depth>0 && - !base_type_eq(t1.subtype(), t2.subtype(), ns)) + if(depth > 0 && t1.subtype() != t2.subtype()) { if(conflict_path.type().id() == ID_pointer) conflict_path = dereference_exprt(conflict_path); @@ -189,7 +187,7 @@ void linkingt::detailed_conflict_report_rec( msg+=id2string(components2[i].get_name())+')'; break; } - else if(!base_type_eq(subtype1, subtype2, ns)) + else if(subtype1 != subtype2) { typedef std::unordered_set type_sett; type_sett parent_types; @@ -313,7 +311,7 @@ void linkingt::detailed_conflict_report_rec( msg+=std::to_string(parameters1.size())+'/'; msg+=std::to_string(parameters2.size())+')'; } - else if(!base_type_eq(return_type1, return_type2, ns)) + else if(return_type1 != return_type2) { conflict_path= index_exprt(conflict_path, @@ -337,7 +335,7 @@ void linkingt::detailed_conflict_report_rec( const typet &subtype1=parameters1[i].type(); const typet &subtype2=parameters2[i].type(); - if(!base_type_eq(subtype1, subtype2, ns)) + if(subtype1 != subtype2) { conflict_path= index_exprt(conflict_path, @@ -456,7 +454,7 @@ void linkingt::duplicate_code_symbol( symbolt &new_symbol) { // Both are functions. - if(!base_type_eq(old_symbol.type, new_symbol.type, ns)) + if(old_symbol.type != new_symbol.type) { const code_typet &old_t=to_code_type(old_symbol.type); const code_typet &new_t=to_code_type(new_symbol.type); @@ -467,11 +465,8 @@ void linkingt::duplicate_code_symbol( // casts we need to fail hard if(old_symbol.type.get_bool(ID_C_incomplete) && old_symbol.value.is_nil()) { - if(base_type_eq(old_t.return_type(), new_t.return_type(), ns)) - link_warning( - old_symbol, - new_symbol, - "implicit function declaration"); + if(old_t.return_type() == new_t.return_type()) + link_warning(old_symbol, new_symbol, "implicit function declaration"); else link_error( old_symbol, @@ -485,7 +480,7 @@ void linkingt::duplicate_code_symbol( else if( new_symbol.type.get_bool(ID_C_incomplete) && new_symbol.value.is_nil()) { - if(base_type_eq(old_t.return_type(), new_t.return_type(), ns)) + if(old_t.return_type() == new_t.return_type()) link_warning( old_symbol, new_symbol, @@ -497,13 +492,12 @@ void linkingt::duplicate_code_symbol( "implicit function declaration"); } // handle (incomplete) function prototypes - else if(base_type_eq(old_t.return_type(), new_t.return_type(), ns) && - ((old_t.parameters().empty() && - old_t.has_ellipsis() && - old_symbol.value.is_nil()) || - (new_t.parameters().empty() && - new_t.has_ellipsis() && - new_symbol.value.is_nil()))) + else if( + old_t.return_type() == new_t.return_type() && + ((old_t.parameters().empty() && old_t.has_ellipsis() && + old_symbol.value.is_nil()) || + (new_t.parameters().empty() && new_t.has_ellipsis() && + new_symbol.value.is_nil()))) { if(old_t.parameters().empty() && old_t.has_ellipsis() && @@ -553,9 +547,9 @@ void linkingt::duplicate_code_symbol( } // conflicting declarations without a definition, matching return // types - else if(base_type_eq(old_t.return_type(), new_t.return_type(), ns) && - old_symbol.value.is_nil() && - new_symbol.value.is_nil()) + else if( + old_t.return_type() == new_t.return_type() && old_symbol.value.is_nil() && + new_symbol.value.is_nil()) { link_warning( old_symbol, @@ -594,7 +588,7 @@ void linkingt::duplicate_code_symbol( typedef std::deque > conflictst; conflictst conflicts; - if(!base_type_eq(old_t.return_type(), new_t.return_type(), ns)) + if(old_t.return_type() != new_t.return_type()) conflicts.push_back( std::make_pair(old_t.return_type(), new_t.return_type())); @@ -606,7 +600,7 @@ void linkingt::duplicate_code_symbol( n_it!=new_t.parameters().end(); ++o_it, ++n_it) { - if(!base_type_eq(o_it->type(), n_it->type(), ns)) + if(o_it->type() != n_it->type()) conflicts.push_back( std::make_pair(o_it->type(), n_it->type())); } @@ -699,7 +693,7 @@ void linkingt::duplicate_code_symbol( bool found=false; for(const auto &c : union_type.components()) - if(base_type_eq(c.type(), src_type, ns)) + if(c.type() == src_type) { found=true; if(warn_msg.empty()) @@ -774,7 +768,7 @@ void linkingt::duplicate_code_symbol( { // ok, silently ignore } - else if(base_type_eq(old_symbol.type, new_symbol.type, ns)) + else if(old_symbol.type == new_symbol.type) { // keep the one in old_symbol -- libraries come last! warning().source_location=new_symbol.location; @@ -797,7 +791,7 @@ bool linkingt::adjust_object_type_rec( const typet &t2, adjust_type_infot &info) { - if(base_type_eq(t1, t2, ns)) + if(t1 == t2) return false; if( @@ -993,7 +987,7 @@ void linkingt::duplicate_object_symbol( // both are variables bool set_to_new = false; - if(!base_type_eq(old_symbol.type, new_symbol.type, ns)) + if(old_symbol.type != new_symbol.type) { bool failed= adjust_object_type(old_symbol, new_symbol, set_to_new); @@ -1051,7 +1045,7 @@ void linkingt::duplicate_object_symbol( simplify(tmp_old, ns); simplify(tmp_new, ns); - if(base_type_eq(tmp_old, tmp_new, ns)) + if(tmp_old == tmp_new) { // ok, the same } @@ -1176,9 +1170,9 @@ void linkingt::duplicate_type_symbol( return; } - if(old_symbol.type.id()==ID_array && - new_symbol.type.id()==ID_array && - base_type_eq(old_symbol.type.subtype(), new_symbol.type.subtype(), ns)) + if( + old_symbol.type.id() == ID_array && new_symbol.type.id() == ID_array && + old_symbol.type.subtype() == new_symbol.type.subtype()) { if(to_array_type(old_symbol.type).size().is_nil() && to_array_type(new_symbol.type).size().is_not_nil()) @@ -1248,9 +1242,9 @@ bool linkingt::needs_renaming_type( to_union_type(new_symbol.type).is_incomplete()) return false; // not different - if(old_symbol.type.id()==ID_array && - new_symbol.type.id()==ID_array && - base_type_eq(old_symbol.type.subtype(), new_symbol.type.subtype(), ns)) + if( + old_symbol.type.id() == ID_array && new_symbol.type.id() == ID_array && + old_symbol.type.subtype() == new_symbol.type.subtype()) { if(to_array_type(old_symbol.type).size().is_nil() && to_array_type(new_symbol.type).size().is_not_nil()) diff --git a/src/util/Makefile b/src/util/Makefile index d50c5b54322..e51e01990cd 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -2,7 +2,6 @@ SRC = allocate_objects.cpp \ arith_tools.cpp \ array_element_from_pointer.cpp \ array_name.cpp \ - base_type.cpp \ bv_arithmetic.cpp \ byte_operators.cpp \ c_types.cpp \ diff --git a/src/util/base_type.cpp b/src/util/base_type.cpp deleted file mode 100644 index f352a834dbd..00000000000 --- a/src/util/base_type.cpp +++ /dev/null @@ -1,310 +0,0 @@ -/*******************************************************************\ - -Module: Base Type Computation - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Base Type Computation - -#include "base_type.h" - -#include - -#include "namespace.h" -#include "std_types.h" -#include "symbol.h" -#include "union_find.h" - -class base_type_eqt -{ -public: - explicit base_type_eqt(const namespacet &_ns):ns(_ns) - { - } - - bool base_type_eq(const typet &type1, const typet &type2) - { - identifiers.clear(); - return base_type_eq_rec(type1, type2); - } - - bool base_type_eq(const exprt &expr1, const exprt &expr2) - { - identifiers.clear(); - return base_type_eq_rec(expr1, expr2); - } - - virtual ~base_type_eqt() { } - -protected: - const namespacet &ns; - - virtual bool base_type_eq_rec(const typet &type1, const typet &type2); - virtual bool base_type_eq_rec(const exprt &expr1, const exprt &expr2); - - // for loop avoidance - typedef union_find identifierst; - identifierst identifiers; -}; - -void base_type_rec( - typet &type, const namespacet &ns, std::set &symb) -{ - if( - type.id() == ID_c_enum_tag || type.id() == ID_struct_tag || - type.id() == ID_union_tag) - { - const symbolt *symbol; - - if( - !ns.lookup(to_tag_type(type).get_identifier(), symbol) && - symbol->is_type && !symbol->type.is_nil()) - { - type=symbol->type; - base_type_rec(type, ns, symb); // recursive call - return; - } - } - else if(type.id()==ID_array) - { - base_type_rec(to_array_type(type).subtype(), ns, symb); - } - else if(type.id()==ID_struct || - type.id()==ID_union) - { - struct_union_typet::componentst &components= - to_struct_union_type(type).components(); - - for(auto &component : components) - base_type_rec(component.type(), ns, symb); - } - else if(type.id()==ID_pointer) - { - typet &subtype=to_pointer_type(type).subtype(); - - // we need to avoid running into an infinite loop - if( - subtype.id() == ID_c_enum_tag || subtype.id() == ID_struct_tag || - subtype.id() == ID_union_tag) - { - const irep_idt &id = to_tag_type(subtype).get_identifier(); - - if(symb.find(id)!=symb.end()) - return; - - symb.insert(id); - - base_type_rec(subtype, ns, symb); - - symb.erase(id); - } - else - base_type_rec(subtype, ns, symb); - } -} - -void base_type(typet &type, const namespacet &ns) -{ - std::set symb; - base_type_rec(type, ns, symb); -} - -void base_type(exprt &expr, const namespacet &ns) -{ - base_type(expr.type(), ns); - - Forall_operands(it, expr) - base_type(*it, ns); -} - -bool base_type_eqt::base_type_eq_rec( - const typet &type1, - const typet &type2) -{ - if(type1==type2) - return true; - - #if 0 - std::cout << "T1: " << type1.pretty() << '\n'; - std::cout << "T2: " << type2.pretty() << '\n'; - #endif - - // loop avoidance - if( - (type1.id() == ID_c_enum_tag || type1.id() == ID_struct_tag || - type1.id() == ID_union_tag) && - type2.id() == type1.id()) - { - // already in same set? - if(identifiers.make_union( - type1.get(ID_identifier), - type2.get(ID_identifier))) - return true; - } - - if( - type1.id() == ID_c_enum_tag || type1.id() == ID_struct_tag || - type1.id() == ID_union_tag) - { - const symbolt &symbol= - ns.lookup(type1.get(ID_identifier)); - - if(!symbol.is_type) - return false; - - return base_type_eq_rec(symbol.type, type2); - } - - if( - type2.id() == ID_c_enum_tag || type2.id() == ID_struct_tag || - type2.id() == ID_union_tag) - { - const symbolt &symbol= - ns.lookup(type2.get(ID_identifier)); - - if(!symbol.is_type) - return false; - - return base_type_eq_rec(type1, symbol.type); - } - - if(type1.id()!=type2.id()) - return false; - - if(type1.id()==ID_struct || - type1.id()==ID_union) - { - const struct_union_typet::componentst &components1= - to_struct_union_type(type1).components(); - - const struct_union_typet::componentst &components2= - to_struct_union_type(type2).components(); - - if(components1.size()!=components2.size()) - return false; - - for(std::size_t i=0; i