Dirty locals analysis: consume goto_programt instead of goto_functiont

src/analyses/constant_propagator.h

@@ -188,9 +188,8 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
 
   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<constant_propagator_domaint>
     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);

src/analyses/dirty.cpp

@@ -16,9 +16,9 @@ Date: March 2013
 #include <util/pointer_expr.h>
 #include <util/std_expr.h>
 
-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);
 }

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<irep_idt> 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
   {

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)

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);
   }

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());
   }

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{});

src/goto-symex/symex_main.cpp

@@ -448,7 +448,7 @@ std::unique_ptr<goto_symext::statet> 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.

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

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