CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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 "c_types.h"
15#include "std_expr.h"
16#include "symbol_table_base.h"
17
18#include <algorithm>
19
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
50{
51 const symbolt &symbol=lookup(src.get_identifier());
52 CHECK_RETURN(symbol.is_type);
53 CHECK_RETURN(symbol.type.id() == ID_union);
54 return to_union_type(symbol.type);
55}
56
60const struct_typet &
62{
63 const symbolt &symbol=lookup(src.get_identifier());
64 CHECK_RETURN(symbol.is_type);
65 CHECK_RETURN(symbol.type.id() == ID_struct);
66 return to_struct_type(symbol.type);
67}
68
72const c_enum_typet &
74{
75 const symbolt &symbol=lookup(src.get_identifier());
76 CHECK_RETURN(symbol.is_type);
77 CHECK_RETURN(symbol.type.id() == ID_c_enum);
78 return to_c_enum_type(symbol.type);
79}
80
84{
85 const symbolt &symbol = lookup(src.get_identifier());
86 CHECK_RETURN(symbol.is_type);
87 CHECK_RETURN(symbol.type.id() == ID_struct || symbol.type.id() == ID_union);
88 return to_struct_union_type(symbol.type);
89}
90
94{
95 if(expr.id()==ID_symbol)
96 {
97 const symbolt &symbol = lookup(to_symbol_expr(expr));
98
99 if(symbol.is_macro && !symbol.value.is_nil())
100 {
101 expr=symbol.value;
102 follow_macros(expr);
103 }
104
105 return;
106 }
107
108 Forall_operands(it, expr)
109 follow_macros(*it);
110}
111
116std::size_t namespacet::smallest_unused_suffix(const std::string &prefix) const
117{
118 std::size_t m = 0;
119
120 if(symbol_table1!=nullptr)
121 m = std::max(m, symbol_table1->next_unused_suffix(prefix));
122
123 if(symbol_table2!=nullptr)
124 m = std::max(m, symbol_table2->next_unused_suffix(prefix));
125
126 return m;
127}
128
135 const irep_idt &name,
136 const symbolt *&symbol) const
137{
138 symbol_table_baset::symbolst::const_iterator it;
139
140 if(symbol_table1!=nullptr)
141 {
142 it=symbol_table1->symbols.find(name);
143
144 if(it!=symbol_table1->symbols.end())
145 {
146 symbol=&(it->second);
147 return false;
148 }
149 }
150
151 if(symbol_table2!=nullptr)
152 {
153 it=symbol_table2->symbols.find(name);
154
155 if(it!=symbol_table2->symbols.end())
156 {
157 symbol=&(it->second);
158 return false;
159 }
160 }
161
162 return true;
163}
164
168std::size_t
169multi_namespacet::smallest_unused_suffix(const std::string &prefix) const
170{
171 std::size_t m = 0;
172
173 for(const auto &st : symbol_table_list)
174 m = std::max(m, st->next_unused_suffix(prefix));
175
176 return m;
177}
178
186 const irep_idt &name,
187 const symbolt *&symbol) const
188{
189 symbol_table_baset::symbolst::const_iterator s_it;
190
191 for(symbol_table_listt::const_iterator
192 c_it=symbol_table_list.begin();
193 c_it!=symbol_table_list.end();
194 c_it++)
195 {
196 s_it=(*c_it)->symbols.find(name);
197
198 if(s_it!=(*c_it)->symbols.end())
199 {
200 symbol=&(s_it->second);
201 return false;
202 }
203 }
204
205 return true;
206}
const c_enum_typet & to_c_enum_type(const typet &type)
Cast a typet to a c_enum_typet.
Definition c_types.h:335
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition c_types.h:184
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
C enum tag type, i.e., c_enum_typet with an identifier.
Definition c_types.h:352
The type of C enums.
Definition c_types.h:239
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
const irep_idt & id() const
Definition irep.h:388
bool is_nil() const
Definition irep.h:368
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
symbol_table_listt symbol_table_list
Definition namespace.h:169
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition namespace.h:45
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
Definition namespace.cpp:93
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:49
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().
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().
A struct or union tag type.
Definition std_types.h:451
A struct tag type, i.e., struct_typet with an identifier.
Definition std_types.h:493
Structure type, corresponds to C style structs.
Definition std_types.h:231
Base type for structs and unions.
Definition std_types.h:62
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
Symbol table entry.
Definition symbol.h:28
bool is_macro
Definition symbol.h:62
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
A union tag type, i.e., union_typet with an identifier.
Definition c_types.h:199
The union type.
Definition c_types.h:147
#define Forall_operands(it, expr)
Definition expr.h:27
#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:272
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition std_types.h:214
Author: Diffblue Ltd.