diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index b054db09c35..84cf5e1778b 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -188,9 +188,8 @@ class constant_propagator_ait:public ait explicit constant_propagator_ait( const goto_functiont &goto_function, - should_track_valuet should_track_value = track_all_values): - dirty(goto_function), - should_track_value(should_track_value) + should_track_valuet should_track_value = track_all_values) + : dirty(goto_function.body), should_track_value(should_track_value) { } @@ -210,7 +209,7 @@ class constant_propagator_ait:public ait goto_functionst::goto_functiont &goto_function, const namespacet &ns, should_track_valuet should_track_value = track_all_values) - : dirty(goto_function), should_track_value(should_track_value) + : dirty(goto_function.body), should_track_value(should_track_value) { operator()(function_identifier, goto_function, ns); replace(goto_function, ns); diff --git a/src/analyses/dirty.cpp b/src/analyses/dirty.cpp index 11d3b0c3cef..abbb055ef34 100644 --- a/src/analyses/dirty.cpp +++ b/src/analyses/dirty.cpp @@ -16,9 +16,9 @@ Date: March 2013 #include #include -void dirtyt::build(const goto_functiont &goto_function) +void dirtyt::build(const goto_programt &goto_program) { - for(const auto &i : goto_function.body.instructions) + for(const auto &i : goto_program.instructions) { if(i.is_other()) { @@ -108,12 +108,12 @@ void dirtyt::output(std::ostream &out) const /// Analyse the given function with dirtyt if it hasn't been seen before /// \param id: function id to analyse -/// \param function: function to analyse +/// \param goto_program: body of function to analyse void incremental_dirtyt::populate_dirty_for_function( const irep_idt &id, - const goto_functionst::goto_functiont &function) + const goto_programt &goto_program) { auto insert_result = dirty_processed_functions.insert(id); if(insert_result.second) - dirty.add_function(function); + dirty.add_function(goto_program); } diff --git a/src/analyses/dirty.h b/src/analyses/dirty.h index 47a67511c2f..fdb3da0c3a8 100644 --- a/src/analyses/dirty.h +++ b/src/analyses/dirty.h @@ -38,7 +38,6 @@ class dirtyt public: bool initialized; - typedef goto_functionst::goto_functiont goto_functiont; /// \post dirtyt objects that are created through this constructor are not /// safe to use. If you copied a dirtyt (for example, by adding an object @@ -48,9 +47,9 @@ class dirtyt { } - explicit dirtyt(const goto_functiont &goto_function) : initialized(false) + explicit dirtyt(const goto_programt &goto_program) : initialized(false) { - build(goto_function); + build(goto_program); initialized = true; } @@ -81,9 +80,9 @@ class dirtyt return dirty; } - void add_function(const goto_functiont &goto_function) + void add_function(const goto_programt &goto_program) { - build(goto_function); + build(goto_program); initialized = true; } @@ -92,12 +91,12 @@ class dirtyt // dirtyts should not be initialized twice PRECONDITION(!initialized); for(const auto &gf_entry : goto_functions.function_map) - build(gf_entry.second); + build(gf_entry.second.body); initialized = true; } protected: - void build(const goto_functiont &goto_function); + void build(const goto_programt &); // variables whose address is taken std::unordered_set dirty; @@ -119,7 +118,7 @@ class incremental_dirtyt public: void populate_dirty_for_function( const irep_idt &id, - const goto_functionst::goto_functiont &function); + const goto_programt &goto_program); bool operator()(const irep_idt &id) const { diff --git a/src/analyses/local_bitvector_analysis.h b/src/analyses/local_bitvector_analysis.h index 429a1d2ad24..39b6bbcbc90 100644 --- a/src/analyses/local_bitvector_analysis.h +++ b/src/analyses/local_bitvector_analysis.h @@ -27,7 +27,7 @@ class local_bitvector_analysist local_bitvector_analysist( const goto_functiont &_goto_function, const namespacet &ns) - : dirty(_goto_function), + : dirty(_goto_function.body), locals(_goto_function), cfg(_goto_function.body), ns(ns) diff --git a/src/analyses/local_may_alias.h b/src/analyses/local_may_alias.h index 240e004569e..f9f6406a916 100644 --- a/src/analyses/local_may_alias.h +++ b/src/analyses/local_may_alias.h @@ -27,11 +27,10 @@ class local_may_aliast public: typedef goto_functionst::goto_functiont goto_functiont; - explicit local_may_aliast( - const goto_functiont &_goto_function): - dirty(_goto_function), - locals(_goto_function), - cfg(_goto_function.body) + explicit local_may_aliast(const goto_functiont &_goto_function) + : dirty(_goto_function.body), + locals(_goto_function), + cfg(_goto_function.body) { build(_goto_function); } diff --git a/src/goto-instrument/contracts/cfg_info.h b/src/goto-instrument/contracts/cfg_info.h index c8d1c5f1482..1b3b780d47f 100644 --- a/src/goto-instrument/contracts/cfg_info.h +++ b/src/goto-instrument/contracts/cfg_info.h @@ -111,7 +111,7 @@ class function_cfg_infot : public cfg_infot { public: explicit function_cfg_infot(const goto_functiont &_goto_function) - : is_dirty(_goto_function), locals(_goto_function) + : is_dirty(_goto_function.body), locals(_goto_function) { parameters.insert( _goto_function.parameter_identifiers.begin(), @@ -143,7 +143,7 @@ class loop_cfg_infot : public cfg_infot { public: loop_cfg_infot(goto_functiont &_goto_function, const loopt &loop) - : is_dirty(_goto_function) + : is_dirty(_goto_function.body) { for(const auto &t : loop) { @@ -205,10 +205,7 @@ class goto_program_cfg_infot : public cfg_infot goto_program.get_decl_identifiers(locals); // collect dirty locals - goto_functiont goto_function; - goto_function.body.copy_from(goto_program); - - dirtyt is_dirty(goto_function); + dirtyt is_dirty(goto_program); const auto &dirty_ids = is_dirty.get_dirty_ids(); dirty.insert(dirty_ids.begin(), dirty_ids.end()); } diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 096fe555ee4..b41c24bdccf 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -230,7 +230,8 @@ void goto_symext::symex_function_call_post_clean( const goto_functionst::goto_functiont &goto_function = get_goto_function(identifier); - path_storage.dirty.populate_dirty_for_function(identifier, goto_function); + path_storage.dirty.populate_dirty_for_function( + identifier, goto_function.body); auto emplace_safe_pointers_result = path_storage.safe_pointers.emplace(identifier, local_safe_pointerst{}); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index b23e59e0ebc..4acf4a38224 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -448,7 +448,7 @@ std::unique_ptr goto_symext::initialize_entry_point_state( emplace_safe_pointers_result.first->second(start_function->body); path_storage.dirty.populate_dirty_for_function( - entry_point_id, *start_function); + entry_point_id, start_function->body); state->dirty = &path_storage.dirty; // Only enable loop analysis when complexity is enabled. diff --git a/unit/goto-symex/goto_symex_state.cpp b/unit/goto-symex/goto_symex_state.cpp index 1935d184cfb..2afb98b4497 100644 --- a/unit/goto-symex/goto_symex_state.cpp +++ b/unit/goto-symex/goto_symex_state.cpp @@ -48,8 +48,8 @@ SCENARIO( // Initialize dirty field of state incremental_dirtyt dirty; - goto_functiont function; - dirty.populate_dirty_for_function("fun", function); + goto_programt function_body; + dirty.populate_dirty_for_function("fun", function_body); state.dirty = &dirty; GIVEN("An L1 lhs and an L2 rhs of type int") diff --git a/unit/goto-symex/symex_assign.cpp b/unit/goto-symex/symex_assign.cpp index 00e006ff75c..14e0751cf7e 100644 --- a/unit/goto-symex/symex_assign.cpp +++ b/unit/goto-symex/symex_assign.cpp @@ -59,8 +59,8 @@ SCENARIO( // Initialize dirty field of state incremental_dirtyt dirty; - goto_functiont function; - dirty.populate_dirty_for_function("fun", function); + goto_programt function_body; + dirty.populate_dirty_for_function("fun", function_body); state.dirty = &dirty; // Initialize symbol table with an integer symbol `foo`, and a boolean g