CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
fresh_symbol.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Fresh auxiliary symbol creation
4
5Author: 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
33 const typet &type,
34 const std::string &name_prefix,
35 const std::string &basename_prefix,
36 const source_locationt &source_location,
37 const irep_idt &symbol_mode,
38 const namespacet &ns,
39 symbol_table_baset &symbol_table)
40{
41 irep_idt identifier = basename_prefix;
42 std::size_t prefix_size = 0;
43 if(!name_prefix.empty())
44 {
45 identifier = name_prefix + "::" + basename_prefix;
46 prefix_size = name_prefix.size() + 2;
47 }
48 identifier = get_new_name(identifier, ns, '$');
49 std::string basename = id2string(identifier).substr(prefix_size);
50
51 auxiliary_symbolt new_symbol(identifier, type, symbol_mode);
52 new_symbol.base_name = basename;
53 new_symbol.location = source_location;
54 std::pair<symbolt &, bool> res = symbol_table.insert(std::move(new_symbol));
55 CHECK_RETURN(res.second);
56
57 return res.first;
58}
59
72 const typet &type,
73 const std::string &name_prefix,
74 const std::string &basename_prefix,
75 const source_locationt &source_location,
76 const irep_idt &symbol_mode,
77 symbol_table_baset &symbol_table)
78{
80 type,
81 name_prefix,
83 source_location,
84 symbol_mode,
85 namespacet(symbol_table),
86 symbol_table);
87}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition symbol.h:153
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The symbol table base class interface.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
Symbol table entry.
Definition symbol.h:28
source_locationt location
Source code location of definition of symbol.
Definition symbol.h:37
irep_idt irep_idt base_name
Name of module the symbol belongs to.
Definition symbol.h:46
The type of an expression, extends irept.
Definition type.h:29
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)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Fresh auxiliary symbol creation.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
irep_idt get_new_name(const irep_idt &name, const namespacet &ns, char delimiter)
Build and identifier not yet present in the namespace ns based on name.
Definition rename.cpp:16
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
Symbol table entry.
Author: Diffblue Ltd.