diff --git a/src/goto-instrument/cover_filter.cpp b/src/goto-instrument/cover_filter.cpp index 60c6ecf8d1a..03f6b1e2f9e 100644 --- a/src/goto-instrument/cover_filter.cpp +++ b/src/goto-instrument/cover_filter.cpp @@ -29,7 +29,7 @@ bool internal_functions_filtert::operator()( if(function.name == INITIALIZE_FUNCTION) return false; - if(function.is_hidden()) + if(goto_function.is_hidden()) return false; // ignore Java built-ins (synthetic functions) diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index c27057d7df1..5efde5ca4d6 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -226,10 +226,7 @@ void goto_convert_functionst::convert_function( f.body.update(); if(hide(f.body)) - { f.make_hidden(); - symbol_table.get_writeable_ref(identifier).set_hidden(); - } lifetime = parent_lifetime; } diff --git a/src/goto-programs/goto_function.h b/src/goto-programs/goto_function.h index da6d0d35a5e..1856800d4ed 100644 --- a/src/goto-programs/goto_function.h +++ b/src/goto-programs/goto_function.h @@ -60,19 +60,17 @@ class goto_functiont return type.get_bool(ID_C_inlined); } - DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead")) bool is_hidden() const { - return type.get_bool(ID_C_hide); + return function_is_hidden; } - DEPRECATED(SINCE(2019, 2, 16, "Get the type from the symbol table instead")) void make_hidden() { - type.set(ID_C_hide, true); + function_is_hidden = true; } - goto_functiont() : body(), type({}, empty_typet()) + goto_functiont() : body(), type({}, empty_typet()), function_is_hidden(false) { } @@ -81,6 +79,7 @@ class goto_functiont body.clear(); type.clear(); parameter_identifiers.clear(); + function_is_hidden = false; } void swap(goto_functiont &other) @@ -88,6 +87,7 @@ class goto_functiont body.swap(other.body); type.swap(other.type); parameter_identifiers.swap(other.parameter_identifiers); + std::swap(function_is_hidden, other.function_is_hidden); } void copy_from(const goto_functiont &other) @@ -95,6 +95,7 @@ class goto_functiont body.copy_from(other.body); type = other.type; parameter_identifiers = other.parameter_identifiers; + function_is_hidden = other.function_is_hidden; } goto_functiont(const goto_functiont &) = delete; @@ -103,7 +104,8 @@ 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)) + parameter_identifiers(std::move(other.parameter_identifiers)), + function_is_hidden(other.function_is_hidden) { } @@ -112,6 +114,7 @@ class goto_functiont 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; } @@ -120,6 +123,9 @@ class goto_functiont /// The validation mode indicates whether well-formedness check failures are /// reported via DATA_INVARIANT violations or exceptions. void validate(const namespacet &ns, const validation_modet vm) const; + +protected: + bool function_is_hidden; }; void get_local_identifiers(const goto_functiont &, std::set &dest); diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index 8db877b87ab..c86d6e5dd59 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -256,7 +256,7 @@ void goto_inlinet::insert_function_body( end.type=LOCATION; // make sure the inlined function does not introduce hiding - if(ns.lookup(identifier).is_hidden()) + if(goto_function.is_hidden()) { for(auto &instruction : body.instructions) instruction.labels.remove(CPROVER_PREFIX "HIDE"); diff --git a/src/goto-programs/read_bin_goto_object.cpp b/src/goto-programs/read_bin_goto_object.cpp index 7a6015b26ca..9d84f5a5ff9 100644 --- a/src/goto-programs/read_bin_goto_object.cpp +++ b/src/goto-programs/read_bin_goto_object.cpp @@ -131,8 +131,8 @@ static bool read_bin_goto_object( instruction.labels.push_back(label); if(label == CPROVER_PREFIX "HIDE") hidden=true; - // The above info is normally in the type of the goto_functiont object, - // which should likely be stored in the binary. + // The above info is also held in the goto_functiont object, and could + // be stored in the binary. } } @@ -160,15 +160,7 @@ static bool read_bin_goto_object( f.body.update(); if(hidden) - { f.make_hidden(); - // can be removed with the next goto-binary version update as the - // information is guaranteed to be stored in the symbol table -#if GOTO_BINARY_VERSION > 5 -#error This code should be removed -#endif - symbol_table.get_writeable_ref(fname).set_hidden(); - } } functions.compute_location_numbers(); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 69b6daa5d06..ae75fad08fb 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -270,9 +270,8 @@ void goto_symext::symex_function_call_code( [&](const exprt &a) { return state.rename(a, ns); }); // we hide the call if the caller and callee are both hidden - const bool callee_is_hidden = ns.lookup(identifier).is_hidden(); const bool hidden = - state.call_stack().top().hidden_function && callee_is_hidden; + state.call_stack().top().hidden_function && goto_function.is_hidden(); // record the call target.function_call( @@ -338,7 +337,7 @@ void goto_symext::symex_function_call_code( frame.end_of_function=--goto_function.body.instructions.end(); frame.return_value=call.lhs(); frame.function_identifier=identifier; - frame.hidden_function = callee_is_hidden; + frame.hidden_function = goto_function.is_hidden(); const framet &p_frame = state.call_stack().previous_frame(); for(const auto &pair : p_frame.loop_iterations) diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 5e9947116be..68fd360586b 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -434,8 +434,7 @@ std::unique_ptr goto_symext::initialize_entry_point_state( state->call_stack().top().end_of_function = limit; state->call_stack().top().calling_location.pc = state->call_stack().top().end_of_function; - state->call_stack().top().hidden_function = - ns.lookup(entry_point_id).is_hidden(); + state->call_stack().top().hidden_function = start_function->is_hidden(); state->symex_target = ⌖ diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index f6943c80aa7..b7748d7c67c 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -285,7 +285,6 @@ IREP_ID_ONE(signed_int128) IREP_ID_ONE(unsigned_int128) IREP_ID_ONE(case) IREP_ID_TWO(C_inlined, #inlined) -IREP_ID_TWO(C_hide, #hide) IREP_ID_ONE(hide) IREP_ID_ONE(abs) IREP_ID_ONE(sign) diff --git a/src/util/symbol.h b/src/util/symbol.h index d83e7581418..d34c8351c43 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -117,19 +117,6 @@ class symbolt value = exprt(ID_compiled); } - /// Returns true iff the symbol is marked for internal use. - bool is_hidden() const - { - return is_auxiliary; - } - - /// Mark a symbol for internal use. This is advisory and may be utilized, - /// e.g., to filter output. - void set_hidden() - { - is_auxiliary = true; - } - /// Check that a symbol is well formed. bool is_well_formed() const; diff --git a/unit/goto-instrument/cover/cover_only.cpp b/unit/goto-instrument/cover/cover_only.cpp index c6083206108..68c413f7253 100644 --- a/unit/goto-instrument/cover/cover_only.cpp +++ b/unit/goto-instrument/cover/cover_only.cpp @@ -22,7 +22,6 @@ symbolt create_new_symbol(const irep_idt &name, const irep_idt &file_name) source_locationt location; location.set_file(file_name); symbol.location = location; - symbol.type = code_typet{{}, empty_typet{}}; return symbol; }