cprover
Loading...
Searching...
No Matches
namespace.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Namespace
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "namespace.h"
13
14#include <algorithm>
15
16#include "c_types.h"
17#include "std_expr.h"
18#include "symbol_table.h"
19
21{
22}
23
31{
32 return lookup(expr.get_identifier());
33}
34
41const symbolt &namespace_baset::lookup(const tag_typet &type) const
42{
43 return lookup(type.get_identifier());
44}
45
49const typet &namespace_baset::follow(const typet &src) const
50{
51 if(src.id() == ID_union_tag)
52 return follow_tag(to_union_tag_type(src));
53
54 if(src.id() == ID_struct_tag)
57 return src;
58}
59
64{
65 const symbolt &symbol=lookup(src.get_identifier());
66 CHECK_RETURN(symbol.is_type);
67 CHECK_RETURN(symbol.type.id() == ID_union);
68 return to_union_type(symbol.type);
69}
70
74const struct_typet &
76{
77 const symbolt &symbol=lookup(src.get_identifier());
78 CHECK_RETURN(symbol.is_type);
79 CHECK_RETURN(symbol.type.id() == ID_struct);
80 return to_struct_type(symbol.type);
81}
82
86const c_enum_typet &
88{
89 const symbolt &symbol=lookup(src.get_identifier());
90 CHECK_RETURN(symbol.is_type);
91 CHECK_RETURN(symbol.type.id() == ID_c_enum);
92 return to_c_enum_type(symbol.type);
93}
94
98{
99 if(expr.id()==ID_symbol)
100 {
101 const symbolt &symbol = lookup(to_symbol_expr(expr));
102
103 if(symbol.is_macro && !symbol.value.is_nil())
104 {
105 expr=symbol.value;
106 follow_macros(expr);
107 }
108
109 return;
110 }
111
112 Forall_operands(it, expr)
113 follow_macros(*it);
114}
115
120std::size_t namespacet::smallest_unused_suffix(const std::string &prefix) const
121{
122 std::size_t m = 0;
123
124 if(symbol_table1!=nullptr)
125 m = std::max(m, symbol_table1->next_unused_suffix(prefix));
126
127 if(symbol_table2!=nullptr)
128 m = std::max(m, symbol_table2->next_unused_suffix(prefix));
129
130 return m;
131}
132
139 const irep_idt &name,
140 const symbolt *&symbol) const
141{
142 symbol_tablet::symbolst::const_iterator it;
143
144 if(symbol_table1!=nullptr)
145 {
146 it=symbol_table1->symbols.find(name);
147
148 if(it!=symbol_table1->symbols.end())
149 {
150 symbol=&(it->second);
151 return false;
152 }
153 }
154
155 if(symbol_table2!=nullptr)
156 {
157 it=symbol_table2->symbols.find(name);
158
159 if(it!=symbol_table2->symbols.end())
160 {
161 symbol=&(it->second);
162 return false;
163 }
164 }
165
166 return true;
167}
168
172std::size_t
173multi_namespacet::smallest_unused_suffix(const std::string &prefix) const
174{
175 std::size_t m = 0;
176
177 for(const auto &st : symbol_table_list)
178 m = std::max(m, st->next_unused_suffix(prefix));
179
180 return m;
181}
182
190 const irep_idt &name,
191 const symbolt *&symbol) const
192{
193 symbol_tablet::symbolst::const_iterator s_it;
194
195 for(symbol_table_listt::const_iterator
196 c_it=symbol_table_list.begin();
197 c_it!=symbol_table_list.end();
198 c_it++)
199 {
200 s_it=(*c_it)->symbols.find(name);
201
202 if(s_it!=(*c_it)->symbols.end())
203 {
204 symbol=&(s_it->second);
205 return false;
206 }
207 }
208
209 return true;
210}
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition: c_types.h:302
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:162
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:202
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: c_types.h:319
The type of C enums.
Definition: c_types.h:217
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
const irep_idt & id() const
Definition: irep.h:396
bool is_nil() const
Definition: irep.h:376
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:189
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:173
symbol_table_listt symbol_table_list
Definition: namespace.h:169
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:43
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
Definition: namespace.cpp:97
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
virtual ~namespace_baset()
Definition: namespace.cpp:20
const symbol_table_baset * symbol_table1
Definition: namespace.h:129
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
const symbol_table_baset * symbol_table2
Definition: namespace.h:129
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:120
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
Structure type, corresponds to C style structs.
Definition: std_types.h:231
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
std::size_t next_unused_suffix(const std::string &prefix, std::size_t start_number) const
Find smallest unused integer i so that prefix + std::to_string(i) does not exist in the list symbols.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
bool is_macro
Definition: symbol.h:61
bool is_type
Definition: symbol.h:61
typet type
Type of symbol.
Definition: symbol.h:31
exprt value
Initial value of symbol.
Definition: symbol.h:34
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:396
const irep_idt & get_identifier() const
Definition: std_types.h:410
The type of an expression, extends irept.
Definition: type.h:29
A union tag type, i.e., union_typet with an identifier.
Definition: c_types.h:177
The union type.
Definition: c_types.h:125
#define Forall_operands(it, expr)
Definition: expr.h:25
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
Author: Diffblue Ltd.