From 35456a2a690d0694b70b6596b5db1b989c014f93 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 2 Mar 2019 11:21:14 +0000 Subject: [PATCH 1/2] Do not read from goto_functiont::type Future changes will remove this member as it is redundant with the information stored in the symbol table. We keep writing to it so as not to break any users, but no longer read it. --- src/goto-checker/symex_coverage.cpp | 2 +- src/goto-instrument/code_contracts.cpp | 27 ++++++++++--------- .../generate_function_bodies.cpp | 9 ++++--- src/goto-instrument/replace_calls.cpp | 7 ++--- src/goto-programs/goto_convert_functions.cpp | 11 ++++---- src/goto-programs/goto_convert_functions.h | 1 + src/goto-programs/goto_functions.cpp | 12 +++++++++ src/goto-programs/link_goto_model.cpp | 5 ++++ .../remove_function_pointers.cpp | 2 +- src/goto-programs/remove_returns.cpp | 5 ++-- src/goto-symex/symex_function_call.cpp | 4 +-- unit/goto-programs/remove_returns.cpp | 19 ++++++++++--- 12 files changed, 68 insertions(+), 36 deletions(-) diff --git a/src/goto-checker/symex_coverage.cpp b/src/goto-checker/symex_coverage.cpp index e8db1b91788..bb67204a195 100644 --- a/src/goto-checker/symex_coverage.cpp +++ b/src/goto-checker/symex_coverage.cpp @@ -161,7 +161,7 @@ goto_program_coverage_recordt::goto_program_coverage_recordt( xml.set_attribute("name", id2string(gf_it->first)); xml.set_attribute( - "signature", from_type(ns, gf_it->first, gf_it->second.type)); + "signature", from_type(ns, gf_it->first, ns.lookup(gf_it->first).type)); xml.set_attribute("line-rate", rate_detailed(lines_covered, lines_total)); xml.set_attribute("branch-rate", rate(branches_covered, branches_total)); diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index 23a369a2391..acea1aaba91 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -484,8 +484,8 @@ void code_contractst::instrument_call_statement( return; } - exprt called_assigns = static_cast( - called_func->second.type.find(ID_C_spec_assigns)); + exprt called_assigns = + static_cast(called_sym.type.find(ID_C_spec_assigns)); if(called_assigns.is_nil()) // Called function has no assigns clause { // Fail if called function has no assigns clause. @@ -763,18 +763,15 @@ void code_contractst::add_contract_check( { PRECONDITION(!dest.instructions.empty()); - goto_functionst::function_mapt::iterator f_it = - goto_functions.function_map.find(mangled_fun); - PRECONDITION(f_it != goto_functions.function_map.end()); - - const goto_functionst::goto_functiont &gf = f_it->second; + const symbolt &function_symbol = ns.lookup(mangled_fun); + const code_typet &code_type = to_code_type(function_symbol.type); const exprt &assigns = - static_cast(gf.type.find(ID_C_spec_assigns)); + static_cast(code_type.find(ID_C_spec_assigns)); const exprt &requires = - static_cast(gf.type.find(ID_C_spec_requires)); + static_cast(code_type.find(ID_C_spec_requires)); const exprt &ensures = - static_cast(gf.type.find(ID_C_spec_ensures)); + static_cast(code_type.find(ID_C_spec_ensures)); INVARIANT( ensures.is_not_nil() || assigns.is_not_nil(), "Code contract enforcement is trivial without an ensures or assigns " @@ -803,15 +800,14 @@ void code_contractst::add_contract_check( skip->source_location)); // prepare function call including all declarations - const symbolt &function_symbol = ns.lookup(mangled_fun); code_function_callt call(function_symbol.symbol_expr()); replace_symbolt replace; // decl ret - if(gf.type.return_type()!=empty_typet()) + if(code_type.return_type() != empty_typet()) { symbol_exprt r = new_tmp_symbol( - gf.type.return_type(), + code_type.return_type(), skip->source_location, wrapper_fun, function_symbol.mode) @@ -825,6 +821,11 @@ void code_contractst::add_contract_check( } // decl parameter1 ... + goto_functionst::function_mapt::iterator f_it = + goto_functions.function_map.find(mangled_fun); + PRECONDITION(f_it != goto_functions.function_map.end()); + + const goto_functionst::goto_functiont &gf = f_it->second; for(const auto ¶meter : gf.parameter_identifiers) { PRECONDITION(!parameter.empty()); diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index d306546f560..b13a096d726 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -321,9 +321,10 @@ class havoc_generate_function_bodiest : public generate_function_bodiest function.body.destructive_append(dest); } - if(function.type.return_type() != empty_typet()) + const typet &return_type = to_code_type(function_symbol.type).return_type(); + if(return_type != empty_typet()) { - typet type(function.type.return_type()); + typet type(return_type); type.remove(ID_C_constant); symbolt &aux_symbol = get_fresh_aux_symbol( @@ -350,8 +351,8 @@ class havoc_generate_function_bodiest : public generate_function_bodiest function.body.destructive_append(dest); - exprt return_expr = typecast_exprt::conditional_cast( - aux_symbol.symbol_expr(), function.type.return_type()); + exprt return_expr = + typecast_exprt::conditional_cast(aux_symbol.symbol_expr(), return_type); add_instruction(goto_programt::make_return(code_returnt(return_expr))); diff --git a/src/goto-instrument/replace_calls.cpp b/src/goto-instrument/replace_calls.cpp index bcda1f462e9..cc554fa6031 100644 --- a/src/goto-instrument/replace_calls.cpp +++ b/src/goto-instrument/replace_calls.cpp @@ -97,7 +97,7 @@ void replace_callst::operator()( PRECONDITION(base_type_eq(f_it1->second.type, f_it2->second.type, ns)); // check that returns have not been removed - if(to_code_type(f_it1->second.type).return_type().id() != ID_empty) + if(to_code_type(function.type()).return_type().id() != ID_empty) { goto_programt::const_targett next_it = std::next(it); if(next_it != goto_program.instructions.end() && next_it->is_assign()) @@ -112,7 +112,7 @@ void replace_callst::operator()( } // Finally modify the call - function.type() = f_it2->second.type; + function.type() = ns.lookup(f_it2->first).type; se.set_identifier(new_id); ins.set_function_call(cfc); @@ -167,7 +167,8 @@ 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(!base_type_eq( + ns.lookup(it1->first).type, ns.lookup(it2->first).type, ns)) throw invalid_command_line_argument_exceptiont( "functions " + id2string(p.first) + " and " + id2string(p.second) + " are not type-compatible", diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 5efde5ca4d6..9bd15735f39 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -87,6 +87,7 @@ bool goto_convert_functionst::hide(const goto_programt &goto_program) void goto_convert_functionst::add_return( goto_functionst::goto_functiont &f, + const typet &return_type, const source_locationt &source_location) { #if 0 @@ -133,7 +134,7 @@ void goto_convert_functionst::add_return( #endif - side_effect_expr_nondett rhs(f.type.return_type(), source_location); + side_effect_expr_nondett rhs(return_type, source_location); f.body.add( goto_programt::make_return(code_returnt(std::move(rhs)), source_location)); @@ -190,15 +191,15 @@ void goto_convert_functionst::convert_function( targets = targetst(); targets.set_return(end_function); - targets.has_return_value = f.type.return_type().id() != ID_empty && - f.type.return_type().id() != ID_constructor && - f.type.return_type().id() != ID_destructor; + targets.has_return_value = code_type.return_type().id() != ID_empty && + code_type.return_type().id() != ID_constructor && + code_type.return_type().id() != ID_destructor; goto_convert_rec(code, f.body, mode); // add non-det return value, if needed if(targets.has_return_value) - add_return(f, end_location); + add_return(f, code_type.return_type(), end_location); // handle SV-COMP's __VERIFIER_atomic_ if( diff --git a/src/goto-programs/goto_convert_functions.h b/src/goto-programs/goto_convert_functions.h index 537f34ec017..ad26bf80268 100644 --- a/src/goto-programs/goto_convert_functions.h +++ b/src/goto-programs/goto_convert_functions.h @@ -58,6 +58,7 @@ class goto_convert_functionst:public goto_convertt // void add_return( goto_functionst::goto_functiont &, + const typet &return_type, const source_locationt &); }; diff --git a/src/goto-programs/goto_functions.cpp b/src/goto-programs/goto_functions.cpp index 348fc8047e7..f038baac87f 100644 --- a/src/goto-programs/goto_functions.cpp +++ b/src/goto-programs/goto_functions.cpp @@ -137,5 +137,17 @@ void goto_functionst::validate(const namespacet &ns, const validation_modet vm) } goto_function.validate(ns, vm); + + // Check that a void function does not contain any RETURN instructions + if(to_code_type(function_symbol.type).return_type().id() == ID_empty) + { + forall_goto_program_instructions(instruction, goto_function.body) + { + DATA_CHECK( + vm, + !instruction->is_return(), + "void function should not return a value"); + } + } } } diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp index 9d17a208287..c7d2c3f6628 100644 --- a/src/goto-programs/link_goto_model.cpp +++ b/src/goto-programs/link_goto_model.cpp @@ -100,6 +100,11 @@ static bool link_functions( in_dest_symbol_table.parameter_identifiers.swap( src_func.parameter_identifiers); in_dest_symbol_table.type=src_func.type; + // the linking code will have ensured that types match + INVARIANT( + base_type_eq( + dest_symbol_table.lookup_ref(final_id).type, src_func.type, ns), + "linking ensures that types match"); } else if(src_func.body.instructions.empty() || src_ns.lookup(src_it->first).is_weak) diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 3c579f386b1..b11fc63b95e 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -125,7 +125,7 @@ remove_function_pointerst::remove_function_pointerst( // build type map forall_goto_functions(f_it, goto_functions) - type_map.emplace(f_it->first, f_it->second.type); + type_map.emplace(f_it->first, to_code_type(ns.lookup(f_it->first).type)); } bool remove_function_pointerst::arg_is_type_compatible( diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index b93af440f65..ac912dfe3b9 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -101,10 +101,11 @@ void remove_returnst::replace_returns( const irep_idt &function_id, goto_functionst::goto_functiont &function) { - typet return_type = function.type.return_type(); + // look up the function symbol + symbolt &function_symbol = *symbol_table.get_writeable(function_id); // returns something but void? - if(return_type == empty_typet()) + if(to_code_type(function_symbol.type).return_type() == empty_typet()) return; // add return_value symbol to symbol_table, if not already created: diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index ae75fad08fb..ab0c47f4a98 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -42,8 +42,6 @@ void goto_symext::parameter_assignments( statet &state, const exprt::operandst &arguments) { - const code_typet &function_type=goto_function.type; - // iterates over the arguments exprt::operandst::const_iterator it1=arguments.begin(); @@ -151,7 +149,7 @@ void goto_symext::parameter_assignments( it1++; } - if(function_type.has_ellipsis()) + if(to_code_type(ns.lookup(function_identifier).type).has_ellipsis()) { // These are va_arg arguments; their types may differ from call to call for(; it1 != arguments.end(); it1++) diff --git a/unit/goto-programs/remove_returns.cpp b/unit/goto-programs/remove_returns.cpp index 32fd257822b..4d782231d03 100644 --- a/unit/goto-programs/remove_returns.cpp +++ b/unit/goto-programs/remove_returns.cpp @@ -48,11 +48,22 @@ TEST_CASE( { symbol_tablet symbol_table; goto_functionst goto_functions; + + symbolt foo_function_symbol; + foo_function_symbol.name = "foo_function"; + foo_function_symbol.type = code_typet{{}, empty_typet{}}; + symbol_table.insert(foo_function_symbol); + + symbolt bar_function_symbol; + bar_function_symbol.name = "bar_function"; + bar_function_symbol.type = code_typet{{}, signedbv_typet{32}}; + symbol_table.insert(bar_function_symbol); + *goto_functions.function_map["foo_function"].body.add_instruction() = - goto_programt::make_function_call(code_function_callt{ - symbol_exprt{"local_variable", signedbv_typet{32}}, - symbol_exprt{"bar_function", code_typet{{}, signedbv_typet{32}}}, - {}}); + goto_programt::make_function_call( + code_function_callt{symbol_exprt{"local_variable", signedbv_typet{32}}, + bar_function_symbol.symbol_expr(), + {}}); const cbmc_invariants_should_throwt invariants_throw; REQUIRE_THROWS_MATCHES( remove_returns(symbol_table, goto_functions), From 33d85ff4051cc187ff89b265259cd3afa30409fb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 21 Feb 2019 19:45:29 +0000 Subject: [PATCH 2/2] Remove goto_functiont::type Having two function type definitions (one in the symbol table and one in goto_functiont) is just prone to become inconsistent. Instead, always look at the symbol table when we do need type information. If all we care about are the identifiers we can still use goto_functiont::parameter_identifiers. --- src/assembler/remove_asm.cpp | 24 +++---- .../function_call_harness_generator.cpp | 4 -- .../memory_snapshot_harness_generator.cpp | 1 - src/goto-harness/recursive_initialization.cpp | 2 - src/goto-instrument/code_contracts.cpp | 2 - .../generate_function_bodies.cpp | 3 - src/goto-instrument/replace_calls.cpp | 2 - src/goto-programs/goto_convert_functions.cpp | 1 - src/goto-programs/goto_function.cpp | 23 ------- src/goto-programs/goto_function.h | 23 +------ src/goto-programs/goto_functions.cpp | 7 -- src/goto-programs/link_goto_model.cpp | 14 ---- src/goto-programs/read_bin_goto_object.cpp | 5 +- src/goto-programs/remove_complex.cpp | 2 - src/goto-programs/remove_vector.cpp | 2 - unit/Makefile | 1 - .../goto_model_function_type_consistency.cpp | 67 ------------------- 17 files changed, 16 insertions(+), 167 deletions(-) delete mode 100644 unit/goto-programs/goto_model_function_type_consistency.cpp diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp index 4b258382a91..0e4c065077e 100644 --- a/src/assembler/remove_asm.cpp +++ b/src/assembler/remove_asm.cpp @@ -122,14 +122,14 @@ void remove_asmt::gcc_asm_function_call( symbol.mode = ID_C; symbol_table.add(symbol); - } - if( - goto_functions.function_map.find(function_identifier) == - goto_functions.function_map.end()) + goto_functions.function_map.emplace(function_identifier, goto_functiont()); + } + else { - auto &f = goto_functions.function_map[function_identifier]; - f.type = fkt_type; + DATA_INVARIANT( + symbol_table.lookup_ref(function_identifier).type == fkt_type, + "function types should match"); } } @@ -171,14 +171,14 @@ void remove_asmt::msc_asm_function_call( symbol.mode = ID_C; symbol_table.add(symbol); - } - if( - goto_functions.function_map.find(function_identifier) == - goto_functions.function_map.end()) + goto_functions.function_map.emplace(function_identifier, goto_functiont()); + } + else { - auto &f = goto_functions.function_map[function_identifier]; - f.type = fkt_type; + DATA_INVARIANT( + symbol_table.lookup_ref(function_identifier).type == fkt_type, + "function types should match"); } } diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index 8f15d4ee88c..a8ab62f9a40 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -453,10 +453,6 @@ void function_call_harness_generatort::implt:: symbol_table->insert(harness_function_symbol); - auto const &generated_harness = - symbol_table->lookup_ref(harness_function_name); - goto_functions->function_map[harness_function_name].type = - to_code_type(generated_harness.type); goto_convert(*symbol_table, *goto_functions, *message_handler); } diff --git a/src/goto-harness/memory_snapshot_harness_generator.cpp b/src/goto-harness/memory_snapshot_harness_generator.cpp index d4181561145..48df43a378d 100644 --- a/src/goto-harness/memory_snapshot_harness_generator.cpp +++ b/src/goto-harness/memory_snapshot_harness_generator.cpp @@ -322,7 +322,6 @@ void memory_snapshot_harness_generatort:: CHECK_RETURN(function_iterator_pair.second); goto_functiont &harness_function = function_iterator_pair.first->second; - harness_function.type = to_code_type(function.type); goto_convert( goto_model.symbol_table, goto_model.goto_functions, message_handler); diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 2a52d98be29..539ba071be2 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -366,8 +366,6 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr) expr_name, is_nullable); - goto_model.goto_functions.function_map[function_symbol.name].type = - to_code_type(function_symbol.type); return type_constructor_names.at(key); } diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index acea1aaba91..b574ca328d0 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -749,8 +749,6 @@ bool code_contractst::enforce_contract(const std::string &fun_to_enforce) goto_functiont &wrapper = goto_functions.function_map[original]; wrapper.parameter_identifiers = mangled_fun->second.parameter_identifiers; - if(mangled_fun->second.type.is_not_nil()) - wrapper.type = mangled_fun->second.type; wrapper.body.add(goto_programt::make_end_function(sl)); add_contract_check(original, mangled, wrapper.body); return false; diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index b13a096d726..ed79ce35994 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -64,7 +64,6 @@ void generate_function_bodiest::generate_parameter_names( symbol_table.add(new_param_sym); } } - function.type = to_code_type(function_symbol.type); function.set_parameter_identifiers(to_code_type(function_symbol.type)); } @@ -591,8 +590,6 @@ void generate_function_bodies( model.symbol_table.lookup_ref(havoc_function_symbol.name); // convert to get the function stub to goto-model - model.goto_functions.function_map[havoc_function_symbol.name].type = - to_code_type(generated_havoc.type); goto_convert(model.symbol_table, model.goto_functions, message_handler); // now generate body as above diff --git a/src/goto-instrument/replace_calls.cpp b/src/goto-instrument/replace_calls.cpp index cc554fa6031..fe28bea210f 100644 --- a/src/goto-instrument/replace_calls.cpp +++ b/src/goto-instrument/replace_calls.cpp @@ -94,8 +94,6 @@ 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)); - // check that returns have not been removed if(to_code_type(function.type()).return_type().id() != ID_empty) { diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 9bd15735f39..291180060d2 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -155,7 +155,6 @@ void goto_convert_functionst::convert_function( // store the parameter identifiers in the goto functions const code_typet &code_type = to_code_type(symbol.type); - f.type = code_type; f.set_parameter_identifiers(code_type); if( diff --git a/src/goto-programs/goto_function.cpp b/src/goto-programs/goto_function.cpp index 6fa8480a791..43c1badace4 100644 --- a/src/goto-programs/goto_function.cpp +++ b/src/goto-programs/goto_function.cpp @@ -46,27 +46,4 @@ void goto_functiont::validate(const namespacet &ns, const validation_modet vm) } body.validate(ns, vm); - - find_symbols_sett typetags; - find_type_symbols(type, typetags); - const symbolt *symbol; - for(const auto &identifier : typetags) - { - DATA_CHECK( - vm, !ns.lookup(identifier, symbol), id2string(identifier) + " not found"); - } - - // Check that a void function does not contain any RETURN instructions - if(to_code_type(type).return_type().id() == ID_empty) - { - forall_goto_program_instructions(instruction, body) - { - DATA_CHECK( - vm, - !instruction->is_return(), - "void function should not return a value"); - } - } - - validate_full_type(type, ns, vm); } diff --git a/src/goto-programs/goto_function.h b/src/goto-programs/goto_function.h index 1856800d4ed..f8cbdcd4b07 100644 --- a/src/goto-programs/goto_function.h +++ b/src/goto-programs/goto_function.h @@ -16,25 +16,19 @@ Date: May 2018 #include -#include #include #include #include "goto_program.h" -/// A goto function, consisting of function type (see #type), function body (see -/// #body), and parameter identifiers (see #parameter_identifiers). +/// A goto function, consisting of function body (see #body) and parameter +/// identifiers (see #parameter_identifiers). class goto_functiont { public: goto_programt body; - /// The type of the function, indicating the return type and parameter types - DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead")) - code_typet type; - typedef std::vector parameter_identifierst; - /// The identifiers of the parameters of this function /// /// Note: This is now the preferred way of getting the identifiers of the @@ -54,12 +48,6 @@ class goto_functiont parameter_identifiers.push_back(parameter.get_identifier()); } - DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead")) - bool is_inlined() const - { - return type.get_bool(ID_C_inlined); - } - bool is_hidden() const { return function_is_hidden; @@ -70,14 +58,13 @@ class goto_functiont function_is_hidden = true; } - goto_functiont() : body(), type({}, empty_typet()), function_is_hidden(false) + goto_functiont() : body(), function_is_hidden(false) { } void clear() { body.clear(); - type.clear(); parameter_identifiers.clear(); function_is_hidden = false; } @@ -85,7 +72,6 @@ class goto_functiont void swap(goto_functiont &other) { body.swap(other.body); - type.swap(other.type); parameter_identifiers.swap(other.parameter_identifiers); std::swap(function_is_hidden, other.function_is_hidden); } @@ -93,7 +79,6 @@ class goto_functiont void copy_from(const goto_functiont &other) { body.copy_from(other.body); - type = other.type; parameter_identifiers = other.parameter_identifiers; function_is_hidden = other.function_is_hidden; } @@ -103,7 +88,6 @@ class goto_functiont goto_functiont(goto_functiont &&other) : body(std::move(other.body)), - type(std::move(other.type)), parameter_identifiers(std::move(other.parameter_identifiers)), function_is_hidden(other.function_is_hidden) { @@ -112,7 +96,6 @@ class goto_functiont goto_functiont &operator=(goto_functiont &&other) { body = std::move(other.body); - type = std::move(other.type); parameter_identifiers = std::move(other.parameter_identifiers); function_is_hidden = other.function_is_hidden; return *this; diff --git a/src/goto-programs/goto_functions.cpp b/src/goto-programs/goto_functions.cpp index f038baac87f..a26793423af 100644 --- a/src/goto-programs/goto_functions.cpp +++ b/src/goto-programs/goto_functions.cpp @@ -109,13 +109,6 @@ void goto_functionst::validate(const namespacet &ns, const validation_modet vm) const code_typet::parameterst ¶meters = to_code_type(function_symbol.type).parameters(); - DATA_CHECK( - vm, - goto_function.type == ns.lookup(function_name).type, - id2string(function_name) + " type inconsistency\ngoto program type: " + - goto_function.type.id_string() + - "\nsymbol table type: " + ns.lookup(function_name).type.id_string()); - DATA_CHECK( vm, goto_function.parameter_identifiers.size() == parameters.size(), diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp index c7d2c3f6628..22c62f20c7e 100644 --- a/src/goto-programs/link_goto_model.cpp +++ b/src/goto-programs/link_goto_model.cpp @@ -35,7 +35,6 @@ static void rename_symbols_in_function( } goto_programt &program=function.body; - rename_symbol(function.type); Forall_goto_program_instructions(iit, program) { @@ -99,12 +98,6 @@ static bool link_functions( in_dest_symbol_table.body.swap(src_func.body); in_dest_symbol_table.parameter_identifiers.swap( src_func.parameter_identifiers); - in_dest_symbol_table.type=src_func.type; - // the linking code will have ensured that types match - INVARIANT( - base_type_eq( - dest_symbol_table.lookup_ref(final_id).type, src_func.type, ns), - "linking ensures that types match"); } else if(src_func.body.instructions.empty() || src_ns.lookup(src_it->first).is_weak) @@ -115,13 +108,6 @@ static bool link_functions( { // ok, we silently ignore } - else - { - // 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"); - } } } diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index 9d84f5a5ff9..d4dbc11507b 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -74,10 +74,7 @@ static bool read_bin_goto_object( { // makes sure there is an empty function for every function symbol auto entry = functions.function_map.emplace(sym.name, goto_functiont()); - - const code_typet &code_type = to_code_type(sym.type); - entry.first->second.type = code_type; - entry.first->second.set_parameter_identifiers(code_type); + entry.first->second.set_parameter_identifiers(to_code_type(sym.type)); } symbol_table.add(sym); diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp index cc4cf37e2bc..2964efe8500 100644 --- a/src/goto-programs/remove_complex.cpp +++ b/src/goto-programs/remove_complex.cpp @@ -283,8 +283,6 @@ void remove_complex(symbol_tablet &symbol_table) static void remove_complex( goto_functionst::goto_functiont &goto_function) { - remove_complex(goto_function.type); - for(auto &i : goto_function.body.instructions) i.transform([](exprt e) -> optionalt { if(have_to_remove_complex(e)) diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp index 9e3cc01024a..e1e910aa176 100644 --- a/src/goto-programs/remove_vector.cpp +++ b/src/goto-programs/remove_vector.cpp @@ -217,8 +217,6 @@ static void remove_vector(symbol_tablet &symbol_table) /// removes vector data type void remove_vector(goto_functionst::goto_functiont &goto_function) { - remove_vector(goto_function.type); - for(auto &i : goto_function.body.instructions) i.transform([](exprt e) -> optionalt { if(have_to_remove_vector(e)) diff --git a/unit/Makefile b/unit/Makefile index 905b2a47bce..1aeb174b752 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -33,7 +33,6 @@ SRC += analyses/ai/ai.cpp \ goto-checker/report_util/is_property_less_than.cpp \ goto-instrument/cover_instrument.cpp \ goto-instrument/cover/cover_only.cpp \ - goto-programs/goto_model_function_type_consistency.cpp \ goto-programs/goto_program_assume.cpp \ goto-programs/goto_program_dead.cpp \ goto-programs/goto_program_declaration.cpp \ diff --git a/unit/goto-programs/goto_model_function_type_consistency.cpp b/unit/goto-programs/goto_model_function_type_consistency.cpp deleted file mode 100644 index d88e617850c..00000000000 --- a/unit/goto-programs/goto_model_function_type_consistency.cpp +++ /dev/null @@ -1,67 +0,0 @@ -/*******************************************************************\ - -Module: Unit tests for goto_model::validate - -Author: Diffblue Ltd. - -\*******************************************************************/ - -#include - -#include - -#include -#include - -SCENARIO( - "Validation of consistent program/table pair (function type)", - "[core][goto-programs][validate]") -{ - GIVEN("A model with one function") - { - const typet type1 = signedbv_typet(32); - const typet type2 = signedbv_typet(64); - code_typet fun_type1({}, type1); - code_typet fun_type2({}, type2); - - symbolt function_symbol; - function_symbol.mode = "C"; - irep_idt function_symbol_name = "foo"; - function_symbol.name = function_symbol_name; - - goto_modelt goto_model; - goto_model.goto_functions.function_map[function_symbol.name] = - goto_functiont(); - goto_model.goto_functions.function_map[function_symbol.name].type = - fun_type1; - - goto_model_validation_optionst validation_options{ - goto_model_validation_optionst::set_optionst::all_false}; - - WHEN("Symbol table has the right type") - { - function_symbol.type = fun_type1; - goto_model.symbol_table.insert(function_symbol); - - THEN("The consistency check succeeds") - { - goto_model.validate(validation_modet::INVARIANT, validation_options); - - REQUIRE(true); - } - } - - WHEN("Symbol table has the wrong type") - { - function_symbol.type = fun_type2; - goto_model.symbol_table.insert(function_symbol); - - THEN("The consistency check fails") - { - REQUIRE_THROWS_AS( - goto_model.validate(validation_modet::EXCEPTION, validation_options), - incorrect_goto_program_exceptiont); - } - } - } -}