fresh_symbol.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Fresh auxiliary symbol creation
 
Author: Chris Smowton, chris.smowton@diffblue.com
 
\*******************************************************************/
 
 
#include "fresh_symbol.h"
 
#include "invariant.h"
#include "namespace.h"
#include "rename.h"
#include "symbol.h"
#include "symbol_table_base.h"
 
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)
{
  irep_idt identifier = basename_prefix;
  std::size_t prefix_size = 0;
  if(!name_prefix.empty())
  {
    identifier = name_prefix + "::" + basename_prefix;
    prefix_size = name_prefix.size() + 2;
  }
  identifier = get_new_name(identifier, ns, '$');
  std::string basename = id2string(identifier).substr(prefix_size);
 
  auxiliary_symbolt new_symbol(identifier, type, symbol_mode);
  new_symbol.base_name = basename;
  new_symbol.location = source_location;
  std::pair<symbolt &, bool> res = symbol_table.insert(std::move(new_symbol));
  CHECK_RETURN(res.second);
 
  return res.first;
}
 
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);
}