Un-pointer current_names

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

@@ -29,13 +29,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 = new current_namest;
+  current_namest current_names;
 
   /// Counter corresponding to an identifier
-  virtual unsigned current_count(const irep_idt &identifier) const
+  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
@@ -47,7 +47,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);
   }
 };
@@ -88,18 +88,12 @@ struct symex_level2t : public symex_renaming_levelt
 
   optionalt<current_namest> global_names;
 
-  void erase(const irep_idt &identifier)
-  {
-    // We don't want to erase anything from the global scope if it exists.
-    current_names->erase(identifier);
-  }
-
   /// Ages the generation of an ssa expression by one.
   void increase_generation(
     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));
     if (global_names)
       global_names->emplace(l1_identifier, std::make_pair(lhs, 0));
 
@@ -113,8 +107,8 @@ struct symex_level2t : public symex_renaming_levelt
   {
     // If we can't find the name in the local scope, don't increase the global
     // even if it exists there.
-    auto current_names_iter = current_names->find(identifier);
-    if (current_names_iter == current_names->end())
+    auto current_names_iter = current_names.find(identifier);
+    if (current_names_iter == current_names.end())
       return;
 
     // If we have a global store, increment its generation count, then assign
@@ -142,7 +136,7 @@ struct symex_level2t : public symex_renaming_levelt
 
     std::cout << "Printing differences between local and global generations." << '\n';
 
-    for(const auto &local : *current_names)
+    for(const auto &local : current_names)
     {
       auto global_iter = global_names->find(local.first);
       if (global_iter == global_names->end())

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
@@ -361,7 +361,7 @@ static void pop_frame(goto_symext::statet &state)
       }
       auto cur = c_it;
       ++c_it;
-      state.level2.erase(cur->first);
+      state.level2.current_names.erase(cur);
     }
   }
 
@@ -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
-    auto emplace_result = state.level1.current_names->emplace(
+    auto emplace_result = state.level1.current_names.emplace(
       std::piecewise_construct,
       std::forward_as_tuple(lhs.get_l1_object_identifier()),
       std::forward_as_tuple(lhs, 0));