Turn local_names into a pointer

Author: JohnDumbell

src/goto-symex/auto_objects.cpp

@@ -95,8 +95,8 @@ void goto_symext::trigger_auto_object(
       if(has_prefix(id2string(symbol.base_name), "auto_object"))
       {
         // done already?
-        if(state.level2.current_names.find(ssa_expr.get_identifier())==
-           state.level2.current_names.end())
+        if(state.level2.current_names->find(ssa_expr.get_identifier())==
+           state.level2.current_names->end())
         {
           initialize_auto_object(expr, state);
         }

src/goto-symex/renaming_level.cpp

@@ -50,8 +50,8 @@ void symex_level1t::operator()(ssa_exprt &ssa_expr)
 
   const irep_idt l0_name = ssa_expr.get_l1_object_identifier();
 
-  const auto it = current_names.find(l0_name);
-  if(it == current_names.end())
+  const auto it = current_names->find(l0_name);
+  if(it == current_names->end())
     return;
 
   // rename!
@@ -61,14 +61,14 @@ void symex_level1t::operator()(ssa_exprt &ssa_expr)
 void symex_level1t::restore_from(
   const symex_renaming_levelt::current_namest &other)
 {
-  auto it = current_names.begin();
+  auto it = current_names->begin();
   for(const auto &pair : other)
   {
-    while(it != current_names.end() && it->first < pair.first)
+    while(it != current_names->end() && it->first < pair.first)
       ++it;
-    if(it == current_names.end() || pair.first < it->first)
-      current_names.insert(it, pair);
-    else if(it != current_names.end())
+    if(it == current_names->end() || pair.first < it->first)
+      current_names->insert(it, pair);
+    else if(it != current_names->end())
     {
       PRECONDITION(it->first == pair.first);
       it->second = pair.second;

src/goto-symex/renaming_level.h

@@ -30,13 +30,13 @@ struct symex_renaming_levelt
 
   /// Map identifier to ssa_exprt and counter
   typedef std::map<irep_idt, std::pair<ssa_exprt, unsigned>> current_namest;
-  current_namest current_names;
+  current_namest *current_names = new current_namest;
 
   /// Counter corresponding to an identifier
   virtual unsigned current_count(const irep_idt &identifier) const
   {
-    const auto it = current_names.find(identifier);
-    return it == current_names.end() ? 0 : it->second.second;
+    const auto it = current_names->find(identifier);
+    return it == current_names->end() ? 0 : it->second.second;
   }
 
   /// Increase the counter corresponding to an identifier
@@ -48,7 +48,7 @@ struct symex_renaming_levelt
   /// Add the \c ssa_exprt of current_names to vars
   void get_variables(std::unordered_set<ssa_exprt, irep_hash> &vars) const
   {
-    for(const auto &pair : current_names)
+    for(const auto &pair : *current_names)
       vars.insert(pair.second.first);
   }
 };
@@ -93,7 +93,7 @@ struct symex_level2t : public symex_renaming_levelt
 
   void erase(const irep_idt &identifier)
   {
-    current_names.erase(identifier);
+    current_names->erase(identifier);
     if (local_generations)
       local_generations->erase(identifier);
   }
@@ -117,7 +117,7 @@ struct symex_level2t : public symex_renaming_levelt
     const irep_idt l1_identifier,
     const ssa_exprt &lhs)
   {
-    current_names.emplace(l1_identifier, std::make_pair(lhs, 0));
+    current_names->emplace(l1_identifier, std::make_pair(lhs, 0));
     increase_generation(l1_identifier);
   }
 
@@ -126,8 +126,8 @@ struct symex_level2t : public symex_renaming_levelt
   void increase_generation(
     const irep_idt l1_identifier)
   {
-    auto current_names_iter = current_names.find(l1_identifier);
-    if (current_names_iter == current_names.end())
+    auto current_names_iter = current_names->find(l1_identifier);
+    if (current_names_iter == current_names->end())
       return;
 
     current_names_iter->second.second++;
@@ -141,7 +141,7 @@ struct symex_level2t : public symex_renaming_levelt
 
   current_namest get_current_names()
   {
-    return local_generations ? *local_generations : current_names;
+    return local_generations ? *local_generations : *current_names;
   }
 
   void print_differences()

src/goto-symex/symex_function_call.cpp

@@ -346,8 +346,8 @@ static void pop_frame(goto_symext::statet &state)
     state.level1.restore_from(frame.old_level1);
 
     // clear function-locals from L2 renaming
-    for(auto c_it = state.level2.current_names.begin();
-        c_it != state.level2.current_names.end();) // no ++c_it
+    for(auto c_it = state.level2.current_names->begin();
+        c_it != state.level2.current_names->end();) // no ++c_it
     {
       const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
       // could use iteration over local_objects as l1_o_id is prefix
@@ -409,17 +409,17 @@ static void locality(
     const irep_idt l0_name=ssa.get_identifier();
 
     // save old L1 name for popping the frame
-    auto c_it = state.level1.current_names.find(l0_name);
+    auto c_it = state.level1.current_names->find(l0_name);
 
-    if(c_it != state.level1.current_names.end())
+    if(c_it != state.level1.current_names->end())
     {
       frame.old_level1.emplace(l0_name, c_it->second);
       c_it->second = std::make_pair(ssa, frame_nr);
     }
     else
     {
       c_it = state.level1.current_names
-               .emplace(l0_name, std::make_pair(ssa, frame_nr))
+        ->emplace(l0_name, std::make_pair(ssa, frame_nr))
                .first;
     }
 

src/goto-symex/symex_start_thread.cpp

@@ -52,8 +52,8 @@ void goto_symext::symex_start_thread(statet &state)
   // create a copy of the local variables for the new thread
   framet &frame = state.top();
 
-  for(auto c_it = state.level2.current_names.begin();
-      c_it != state.level2.current_names.end();
+  for(auto c_it = state.level2.current_names->begin();
+      c_it != state.level2.current_names->end();
       ++c_it)
   {
     const irep_idt l1_o_id=c_it->second.first.get_l1_object_identifier();
@@ -68,7 +68,7 @@ void goto_symext::symex_start_thread(statet &state)
     lhs.set_level_0(t);
 
     // set up L1 name
-    if(!state.level1.current_names.insert(
+    if(!state.level1.current_names->insert(
         std::make_pair(lhs.get_l1_object_identifier(),
                        std::make_pair(lhs, 0))).second)
       UNREACHABLE;