Cleanup and correctly document get_new_name

Remove the unused variant that takes a symbol as first argument. Change
the interface to explicitly return a value. Add proper doxygen
documentation rather than accepting warnings about wrong documentation.

Author: tautschnig

scripts/expected_doxygen_warnings.txt

@@ -14,10 +14,6 @@
   template
   satcheck_minisat2_baset< Minisat::SimpSolver >::~satcheck_minisat2_baset()
 
-/home/runner/work/cbmc/cbmc/src/util/rename.cpp:27: warning: documented empty return type of get_new_name
-/home/runner/work/cbmc/cbmc/src/util/rename.cpp:19: warning: documented empty return type of get_new_name
-/home/runner/work/cbmc/cbmc/src/util/rename.h:26: warning: documented empty return type of get_new_name
-/home/runner/work/cbmc/cbmc/src/util/rename.h:23: warning: documented empty return type of get_new_name
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/goto-harness/recursive_initialization.cpp

@@ -558,9 +558,8 @@ const symbolt &recursive_initializationt::get_fresh_fun_symbol(
   const std::string &fun_name,
   const typet &fun_type)
 {
-  irep_idt fresh_name(fun_name);
-
-  get_new_name(fresh_name, namespacet{goto_model.symbol_table}, '_');
+  irep_idt fresh_name =
+    get_new_name(fun_name, namespacet{goto_model.symbol_table}, '_');
 
   // create the function symbol
   symbolt function_symbol{};

src/util/fresh_symbol.cpp

@@ -45,7 +45,7 @@ symbolt &get_fresh_aux_symbol(
     identifier = name_prefix + "::" + basename_prefix;
     prefix_size = name_prefix.size() + 2;
   }
-  get_new_name(identifier, ns, '$');
+  identifier = get_new_name(identifier, ns, '$');
   std::string basename = id2string(identifier).substr(prefix_size);
 
   auxiliary_symbolt new_symbol(basename, type);

src/util/rename.cpp

@@ -10,27 +10,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <string>
 
-#include "symbol.h"
 #include "namespace.h"
 
-/// automated variable renaming
-/// \par parameters: symbol to be renamed, namespace
-/// \return new symbol
-void get_new_name(symbolt &symbol, const namespacet &ns)
-{
-  get_new_name(symbol.name, ns);
-}
-
-/// automated variable renaming
-/// \par parameters: symbol to be renamed, namespace
-/// \return new symbol
-void get_new_name(irep_idt &new_name, const namespacet &ns, char delimiter)
+irep_idt
+get_new_name(const irep_idt &name, const namespacet &ns, char delimiter)
 {
   const symbolt *symbol;
-  if(ns.lookup(new_name, symbol))
-    return; // name not taken yet
+  if(ns.lookup(name, symbol))
+    return name;
 
-  std::string prefix = id2string(new_name) + delimiter;
+  std::string prefix = id2string(name) + delimiter;
 
-  new_name = prefix + std::to_string(ns.smallest_unused_suffix(prefix));
+  return prefix + std::to_string(ns.smallest_unused_suffix(prefix));
 }

src/util/rename.h

@@ -15,17 +15,19 @@ Author: Daniel Kroening, kroening@kroening.com
 //
 
 #include "irep.h"
+#include "nodiscard.h"
 
 class exprt;
 class namespacet;
-class symbolt;
 
-void get_new_name(symbolt &symbol,
-                  const namespacet &ns);
-
-void get_new_name(
-  irep_idt &new_name,
-  const namespacet &ns,
-  char delimiter = '_');
+/// Build and identifier not yet present in the namespace \p ns based on \p
+/// name. If \p name is not in the namespace, just returns \p name.
+/// \param name: initial candidate identifier
+/// \param ns: namespace
+/// \param delimiter: character to separate the name and a newly generated
+///   suffix
+/// \return Identifier that is not yet part of the namespace.
+NODISCARD irep_idt
+get_new_name(const irep_idt &name, const namespacet &ns, char delimiter = '_');
 
 #endif // CPROVER_UTIL_RENAME_H