cprover
symbol_table.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "symbol_table.h"
10 
11 #include <ostream>
12 
18 bool symbol_tablet::add(const symbolt &symbol)
19 {
20  if(!symbols.insert(std::pair<irep_idt, symbolt>(symbol.name, symbol)).second)
21  return true;
22 
23  symbol_base_map.insert(
24  std::pair<irep_idt, irep_idt>(symbol.base_name, symbol.name));
25  symbol_module_map.insert(
26  std::pair<irep_idt, irep_idt>(symbol.module, symbol.name));
27 
28  return false;
29 }
30 
46 bool symbol_tablet::move(symbolt &symbol, symbolt *&new_symbol)
47 {
48  symbolt tmp;
49 
50  std::pair<symbolst::iterator, bool> result=
51  symbols.insert(std::pair<irep_idt, symbolt>(symbol.name, tmp));
52 
53  if(!result.second)
54  {
55  new_symbol=&result.first->second;
56  return true;
57  }
58 
59  symbol_base_map.insert(
60  std::pair<irep_idt, irep_idt>(symbol.base_name, symbol.name));
61  symbol_module_map.insert(
62  std::pair<irep_idt, irep_idt>(symbol.module, symbol.name));
63 
64  result.first->second.swap(symbol);
65  new_symbol=&result.first->second;
66 
67  return false;
68 }
69 
74 {
75  symbolst::iterator entry=symbols.find(name);
76 
77  if(entry==symbols.end())
78  return true;
79 
80  for(symbol_base_mapt::iterator
81  it=symbol_base_map.lower_bound(entry->second.base_name),
82  it_end=symbol_base_map.upper_bound(entry->second.base_name);
83  it!=it_end;
84  ++it)
85  if(it->second==name)
86  {
87  symbol_base_map.erase(it);
88  break;
89  }
90 
91  for(symbol_module_mapt::iterator
92  it=symbol_module_map.lower_bound(entry->second.module),
93  it_end=symbol_module_map.upper_bound(entry->second.module);
94  it!=it_end;
95  ++it)
96  if(it->second==name)
97  {
98  symbol_module_map.erase(it);
99  break;
100  }
101 
102  symbols.erase(entry);
103 
104  return false;
105 }
106 
109 void symbol_tablet::show(std::ostream &out) const
110 {
111  out << "\n" << "Symbols:" << "\n";
112 
114  out << it->second;
115 }
116 
121 const symbolt &symbol_tablet::lookup(const irep_idt &identifier) const
122 {
123  symbolst::const_iterator it=symbols.find(identifier);
124 
125  if(it==symbols.end())
126  throw "symbol "+id2string(identifier)+" not found";
127 
128  return it->second;
129 }
130 
136 {
137  symbolst::iterator it=symbols.find(identifier);
138 
139  if(it==symbols.end())
140  throw "symbol "+id2string(identifier)+" not found";
141 
142  return it->second;
143 }
144 
148 std::ostream &operator << (std::ostream &out, const symbol_tablet &symbol_table)
149 {
150  symbol_table.show(out);
151  return out;
152 }
irep_idt name
The unique identifier.
Definition: symbol.h:46
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
std::ostream & operator<<(std::ostream &out, const symbol_tablet &symbol_table)
Print the contents of the symbol table.
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:49
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
symbol_base_mapt symbol_base_map
Definition: symbol_table.h:58
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
symbol_module_mapt symbol_module_map
Definition: symbol_table.h:59
symbolst symbols
Definition: symbol_table.h:57
The symbol table.
Definition: symbol_table.h:52
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Symbol table.
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
void show(std::ostream &out) const
Print the contents of the symbol table.
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52