Create aux symbol with a different name than symbols in namespace

This adds another version of get_fresh_aux_symbol which takes a namespace and
produces symbol names that are different from any of the symbols in the
namespace. This can be used to e.g. generate fresh symbols during symex that
don't clash with any of the existing symbols.

Author: danpoe

src/util/fresh_symbol.cpp

@@ -17,14 +17,16 @@ Author: Chris Smowton, [email protected]
 #include "symbol.h"
 #include "symbol_table_base.h"
 
-/// Installs a fresh-named symbol with the requested name pattern.
+/// Installs a fresh-named symbol with respect to the given namespace `ns` with
+/// the requested name pattern in the given symbol table
 /// \param type: The type of the new symbol.
 /// \param name_prefix: The new symbol will be named
 ///   `name_prefix::basename_prefix$num` unless name_prefix is empty, in which
 ///   case the :: prefix is omitted.
 /// \param basename_prefix: See `name_prefix`.
 /// \param source_location: The source location for the new symbol.
 /// \param symbol_mode: The mode for the new symbol, e.g. ID_C, ID_java.
+/// \param ns: the new symbol has a different name than any symbols in `ns`
 /// \param symbol_table: The symbol table to add the new symbol to.
 /// \return The new symbol.
 symbolt &get_fresh_aux_symbol(
@@ -33,9 +35,9 @@ symbolt &get_fresh_aux_symbol(
   const std::string &basename_prefix,
   const source_locationt &source_location,
   const irep_idt &symbol_mode,
+  const namespacet &ns,
   symbol_table_baset &symbol_table)
 {
-  namespacet ns(symbol_table);
   irep_idt identifier = basename_prefix;
   std::size_t prefix_size = 0;
   if(!name_prefix.empty())
@@ -55,3 +57,32 @@ symbolt &get_fresh_aux_symbol(
 
   return res.first;
 }
+
+/// Installs a fresh-named symbol with the requested name pattern in the given
+/// symbol table
+/// \param type: The type of the new symbol.
+/// \param name_prefix: The new symbol will be named
+///   `name_prefix::basename_prefix$num` unless name_prefix is empty, in which
+///   case the :: prefix is omitted.
+/// \param basename_prefix: See `name_prefix`.
+/// \param source_location: The source location for the new symbol.
+/// \param symbol_mode: The mode for the new symbol, e.g. ID_C, ID_java.
+/// \param symbol_table: The symbol table to add the new symbol to.
+/// \return The new symbol.
+symbolt &get_fresh_aux_symbol(
+  const typet &type,
+  const std::string &name_prefix,
+  const std::string &basename_prefix,
+  const source_locationt &source_location,
+  const irep_idt &symbol_mode,
+  symbol_table_baset &symbol_table)
+{
+  return get_fresh_aux_symbol(
+    type,
+    name_prefix,
+    basename_prefix,
+    source_location,
+    symbol_mode,
+    namespacet(symbol_table),
+    symbol_table);
+}

src/util/fresh_symbol.h

@@ -16,6 +16,7 @@ Author: Chris Smowton, [email protected]
 
 #include "irep.h"
 
+class namespacet;
 class source_locationt;
 class symbolt;
 class symbol_table_baset;
@@ -29,4 +30,13 @@ symbolt &get_fresh_aux_symbol(
   const irep_idt &symbol_mode,
   symbol_table_baset &symbol_table);
 
+symbolt &get_fresh_aux_symbol(
+  const typet &type,
+  const std::string &name_prefix,
+  const std::string &basename_prefix,
+  const source_locationt &source_location,
+  const irep_idt &symbol_mode,
+  const namespacet &ns,
+  symbol_table_baset &symbol_table);
+
 #endif // CPROVER_UTIL_FRESH_SYMBOL_H