Consistently use get_fresh_aux_symbol instead of local implementations

Author: tautschnig

src/goto-programs/goto_convert.cpp

@@ -2058,15 +2058,6 @@ void goto_convertt::make_temp_symbol(
   expr=new_symbol.symbol_expr();
 }
 
-void goto_convertt::new_name(symbolt &symbol)
-{
-  // rename it
-  get_new_name(symbol, ns);
-
-  // store in symbol_table
-  symbol_table.add(symbol);
-}
-
 void goto_convert(
   const codet &code,
   symbol_table_baset &symbol_table,

src/goto-programs/goto_convert_class.h

@@ -56,8 +56,6 @@ class goto_convertt:public messaget
   //
   // tools for symbols
   //
-  void new_name(symbolt &symbol);
-
   symbolt &new_tmp_symbol(
     const typet &type,
     const std::string &suffix,

src/goto-programs/goto_convert_functions.cpp

@@ -147,7 +147,7 @@ void goto_convert_functionst::convert_function(
     return; // already converted
 
   // make tmp variables local to function
-  tmp_symbol_prefix=id2string(symbol.name)+"::$tmp::";
+  tmp_symbol_prefix=id2string(symbol.name)+"::$tmp";
 
   f.type=to_code_type(symbol.type);
 

src/goto-programs/goto_convert_side_effect.cpp

@@ -12,10 +12,10 @@ Author: Daniel Kroening, [email protected]
 #include "goto_convert_class.h"
 
 #include <util/arith_tools.h>
+#include <util/cprover_prefix.h>
 #include <util/expr_util.h>
+#include <util/fresh_symbol.h>
 #include <util/std_expr.h>
-#include <util/rename.h>
-#include <util/cprover_prefix.h>
 #include <util/symbol.h>
 
 #include <util/c_types.h>
@@ -351,12 +351,6 @@ void goto_convertt::remove_function_call(
     return;
   }
 
-  auxiliary_symbolt new_symbol;
-
-  new_symbol.base_name="return_value";
-  new_symbol.type=expr.type();
-  new_symbol.location=expr.find_source_location();
-
   // get name of function, if available
 
   if(expr.id()!=ID_side_effect ||
@@ -374,25 +368,26 @@ void goto_convertt::remove_function_call(
     throw 0;
   }
 
+  std::string new_base_name = "return_value";
+  irep_idt new_symbol_mode = mode;
+
   if(expr.op0().id()==ID_symbol)
   {
     const irep_idt &identifier=expr.op0().get(ID_identifier);
     const symbolt &symbol = ns.lookup(identifier);
 
-    std::string new_base_name=id2string(new_symbol.base_name);
-
     new_base_name+='_';
     new_base_name+=id2string(symbol.base_name);
-    new_base_name += "$0";
-
-    new_symbol.base_name=new_base_name;
-    new_symbol.mode=symbol.mode;
+    new_symbol_mode = symbol.mode;
   }
 
-  new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
-
-  // ensure that the name is unique
-  new_name(new_symbol);
+  const symbolt &new_symbol = get_fresh_aux_symbol(
+    expr.type(),
+    tmp_symbol_prefix,
+    new_base_name,
+    expr.find_source_location(),
+    new_symbol_mode,
+    symbol_table);
 
   {
     code_declt decl;
@@ -432,15 +427,13 @@ void goto_convertt::remove_cpp_new(
 {
   codet call;
 
-  auxiliary_symbolt new_symbol;
-
-  new_symbol.base_name = "new_ptr$0";
-  new_symbol.type=expr.type();
-  new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
-  new_symbol.mode = ID_cpp;
-
-  // ensure that the name is unique
-  new_name(new_symbol);
+  const symbolt &new_symbol = get_fresh_aux_symbol(
+    expr.type(),
+    tmp_symbol_prefix,
+    "new_ptr",
+    expr.find_source_location(),
+    ID_cpp,
+    symbol_table);
 
   code_declt decl;
   decl.symbol()=new_symbol.symbol_expr();
@@ -486,19 +479,15 @@ void goto_convertt::remove_malloc(
 
   if(result_is_used)
   {
-    auxiliary_symbolt new_symbol;
-
-    new_symbol.base_name = "malloc_value$0";
-    new_symbol.type=expr.type();
-    new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
-    new_symbol.location=expr.source_location();
-    new_symbol.mode = mode;
+    const symbolt &new_symbol = get_fresh_aux_symbol(
+      expr.type(),
+      tmp_symbol_prefix,
+      "malloc_value",
+      expr.source_location(),
+      mode,
+      symbol_table);
 
-    // ensure that the name is unique
-    new_name(new_symbol);
-
-    code_declt decl;
-    decl.symbol()=new_symbol.symbol_expr();
+    code_declt decl(new_symbol.symbol_expr());
     decl.add_source_location()=new_symbol.location;
     convert_decl(decl, dest, mode);
 

src/pointer-analysis/value_set_dereference.cpp

@@ -24,11 +24,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/format_type.h>
+#include <util/fresh_symbol.h>
 #include <util/guard.h>
 #include <util/options.h>
 #include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
-#include <util/rename.h>
 #include <util/ssa_expr.h>
 
 #include <ansi-c/c_typecast.h>
@@ -148,22 +148,19 @@ exprt value_set_dereferencet::dereference(
     else
     {
       // else: produce new symbol
-
-      symbolt symbol;
-      symbol.name="symex::invalid_object"+std::to_string(invalid_counter++);
-      symbol.base_name="invalid_object";
-      symbol.type=type;
-      symbol.mode = language_mode;
+      symbolt &symbol = get_fresh_aux_symbol(
+        type,
+        "symex",
+        "invalid_object",
+        pointer.source_location(),
+        language_mode,
+        new_symbol_table);
 
       // make it a lvalue, so we can assign to it
       symbol.is_lvalue=true;
 
-      get_new_name(symbol, ns);
-
       failure_value=symbol.symbol_expr();
       failure_value.set(ID_C_invalid_object, true);
-
-      new_symbol_table.insert(std::move(symbol));
     }
 
     valuet value;