Merge pull request #4925 from danpoe/feature/get-fresh-symbol-in-namespace

Create auxiliary symbols with a different name than symbols in namespace [blocks: #4885]

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