cprover
namespace.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Namespace
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "namespace.h"
13 
14 #include <algorithm>
15 
16 #include <cassert>
17 
18 #include "string2int.h"
19 #include "symbol_table.h"
20 #include "prefix.h"
21 #include "std_types.h"
22 
23 unsigned get_max(
24  const std::string &prefix,
25  const symbol_tablet::symbolst &symbols)
26 {
27  unsigned max_nr=0;
28 
29  forall_symbols(it, symbols)
30  if(has_prefix(id2string(it->first), prefix))
31  max_nr=
32  std::max(unsafe_string2unsigned(
33  id2string(it->first).substr(prefix.size())),
34  max_nr);
35 
36  return max_nr;
37 }
38 
40 {
41 }
42 
44 {
45  while(irep.id()==ID_symbol)
46  {
47  const symbolt &symbol=lookup(irep);
48 
49  if(symbol.is_type)
50  {
51  if(symbol.type.is_nil())
52  return;
53  else
54  irep=symbol.type;
55  }
56  else
57  {
58  if(symbol.value.is_nil())
59  return;
60  else
61  irep=symbol.value;
62  }
63  }
64 }
65 
66 const typet &namespace_baset::follow(const typet &src) const
67 {
68  if(src.id()!=ID_symbol)
69  return src;
70 
71  const symbolt *symbol=&lookup(src);
72 
73  // let's hope it's not cyclic...
74  while(true)
75  {
76  assert(symbol->is_type);
77  if(symbol->type.id()!=ID_symbol)
78  return symbol->type;
79  symbol=&lookup(symbol->type);
80  }
81 }
82 
84 {
85  const symbolt &symbol=lookup(src.get_identifier());
86  assert(symbol.is_type);
87  assert(symbol.type.id()==ID_union || symbol.type.id()==ID_incomplete_union);
88  return symbol.type;
89 }
90 
92 {
93  const symbolt &symbol=lookup(src.get_identifier());
94  assert(symbol.is_type);
95  assert(symbol.type.id()==ID_struct || symbol.type.id()==ID_incomplete_struct);
96  return symbol.type;
97 }
98 
100 {
101  const symbolt &symbol=lookup(src.get_identifier());
102  assert(symbol.is_type);
103  assert(symbol.type.id()==ID_c_enum || symbol.type.id()==ID_incomplete_c_enum);
104  return symbol.type;
105 }
106 
108 {
109  if(expr.id()==ID_symbol)
110  {
111  const symbolt &symbol=lookup(expr);
112 
113  if(symbol.is_macro && !symbol.value.is_nil())
114  {
115  expr=symbol.value;
116  follow_macros(expr);
117  }
118 
119  return;
120  }
121 
122  Forall_operands(it, expr)
123  follow_macros(*it);
124 }
125 
126 unsigned namespacet::get_max(const std::string &prefix) const
127 {
128  unsigned m=0;
129 
130  if(symbol_table1!=nullptr)
131  m=std::max(m, ::get_max(prefix, symbol_table1->symbols));
132 
133  if(symbol_table2!=nullptr)
134  m=std::max(m, ::get_max(prefix, symbol_table2->symbols));
135 
136  return m;
137 }
138 
140  const irep_idt &name,
141  const symbolt *&symbol) const
142 {
143  symbol_tablet::symbolst::const_iterator it;
144 
145  if(symbol_table1!=nullptr)
146  {
147  it=symbol_table1->symbols.find(name);
148 
149  if(it!=symbol_table1->symbols.end())
150  {
151  symbol=&(it->second);
152  return false;
153  }
154  }
155 
156  if(symbol_table2!=nullptr)
157  {
158  it=symbol_table2->symbols.find(name);
159 
160  if(it!=symbol_table2->symbols.end())
161  {
162  symbol=&(it->second);
163  return false;
164  }
165  }
166 
167  return true;
168 }
169 
170 unsigned multi_namespacet::get_max(const std::string &prefix) const
171 {
172  unsigned m=0;
173 
174  for(symbol_table_listt::const_iterator
175  it=symbol_table_list.begin();
176  it!=symbol_table_list.end();
177  it++)
178  m=std::max(m, ::get_max(prefix, (*it)->symbols));
179 
180  return m;
181 }
182 
184  const irep_idt &name,
185  const symbolt *&symbol) const
186 {
187  symbol_tablet::symbolst::const_iterator s_it;
188 
189  for(symbol_table_listt::const_iterator
190  c_it=symbol_table_list.begin();
191  c_it!=symbol_table_list.end();
192  c_it++)
193  {
194  s_it=(*c_it)->symbols.find(name);
195 
196  if(s_it!=(*c_it)->symbols.end())
197  {
198  symbol=&(s_it->second);
199  return false;
200  }
201  }
202 
203  return true;
204 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
const irep_idt & get_identifier() const
Definition: std_types.h:479
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
exprt value
Initial value of symbol.
Definition: symbol.h:40
A union tag type.
Definition: std_types.h:554
A struct tag type.
Definition: std_types.h:517
virtual unsigned get_max(const std::string &prefix) const =0
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
virtual unsigned get_max(const std::string &prefix) const
Definition: namespace.cpp:170
const symbolt & lookup(const irep_idt &name) const
Definition: namespace.h:30
virtual ~namespace_baset()
Definition: namespace.cpp:39
const typet & follow_tag(const union_tag_typet &src) const
Definition: namespace.cpp:83
void follow_macros(exprt &expr) const
Definition: namespace.cpp:107
const irep_idt & id() const
Definition: irep.h:189
std::unordered_map< irep_idt, symbolt, irep_id_hash > symbolst
Definition: symbol_table.h:55
unsigned get_max(const std::string &prefix, const symbol_tablet::symbolst &symbols)
Definition: namespace.cpp:23
Base class for tree-like data structures with sharing.
Definition: irep.h:87
Symbol table.
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
typet type
Type of symbol.
Definition: symbol.h:37
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:183
void follow_symbol(irept &irep) const
Definition: namespace.cpp:43
API to type classes.
Base class for all expressions.
Definition: expr.h:46
#define Forall_operands(it, expr)
Definition: expr.h:23
bool is_type
Definition: symbol.h:66
An enum tag type.
Definition: std_types.h:698
virtual unsigned get_max(const std::string &prefix) const
Definition: namespace.cpp:126
bool is_macro
Definition: symbol.h:66