cprover
fresh_symbol.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Fresh auxiliary symbol creation
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #include "fresh_symbol.h"
13 
14 #include "invariant.h"
15 #include "namespace.h"
16 #include "rename.h"
17 #include "symbol.h"
18 #include "symbol_table_base.h"
19 
31  const typet &type,
32  const std::string &name_prefix,
33  const std::string &basename_prefix,
34  const source_locationt &source_location,
35  const irep_idt &symbol_mode,
36  symbol_table_baset &symbol_table)
37 {
38  namespacet ns(symbol_table);
39  irep_idt identifier = basename_prefix;
40  std::size_t prefix_size = 0;
41  if(!name_prefix.empty())
42  {
43  identifier = name_prefix + "::" + basename_prefix;
44  prefix_size = name_prefix.size() + 2;
45  }
46  get_new_name(identifier, ns, '$');
47  std::string basename = id2string(identifier).substr(prefix_size);
48 
49  auxiliary_symbolt new_symbol(basename, type);
50  new_symbol.name = identifier;
51  new_symbol.location = source_location;
52  new_symbol.mode = symbol_mode;
53  std::pair<symbolt &, bool> res = symbol_table.insert(std::move(new_symbol));
54  CHECK_RETURN(res.second);
55 
56  return res.first;
57 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
get_new_name
void get_new_name(symbolt &symbol, const namespacet &ns)
automated variable renaming
Definition: rename.cpp:19
typet
The type of an expression, extends irept.
Definition: type.h:27
fresh_symbol.h
get_fresh_aux_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)
Installs a fresh-named symbol with the requested name pattern.
Definition: fresh_symbol.cpp:30
invariant.h
auxiliary_symbolt
Internally generated symbol table entry.
Definition: symbol.h:148
namespace.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
rename.h
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
symbol.h
Symbol table entry.
source_locationt
Definition: source_location.h:20
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
symbolt
Symbol table entry.
Definition: symbol.h:27
symbol_table_baset::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
symbol_table_base.h
Author: Diffblue Ltd.
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
dstringt::size
size_t size() const
Definition: dstring.h:91
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470