cprover
Loading...
Searching...
No Matches
namespace.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#ifndef CPROVER_UTIL_NAMESPACE_H
11#define CPROVER_UTIL_NAMESPACE_H
12
13#include "invariant.h"
14#include "irep.h"
15
16class exprt;
17class symbolt;
18class typet;
19class symbol_exprt;
20class tag_typet;
21class union_typet;
22class struct_typet;
23class c_enum_typet;
24class union_tag_typet;
28
34{
35public:
36 // service methods
37
43 const symbolt &lookup(const irep_idt &name) const
44 {
45 const symbolt *symbol;
46 bool not_found = lookup(name, symbol);
48 !not_found,
49 "we are assuming that a name exists in the namespace "
50 "when this function is called - identifier " +
51 id2string(name) + " was not found");
52 return *symbol;
53 }
54
55 const symbolt &lookup(const symbol_exprt &) const;
56 const symbolt &lookup(const tag_typet &) const;
57
58 virtual ~namespace_baset();
59
60 void follow_macros(exprt &) const;
61 const typet &follow(const typet &) const;
62
63 // These produce union_typet, struct_typet, c_enum_typet or
64 // the incomplete version.
65 const union_typet &follow_tag(const union_tag_typet &) const;
66 const struct_typet &follow_tag(const struct_tag_typet &) const;
67 const c_enum_typet &follow_tag(const c_enum_tag_typet &) const;
68
73 virtual std::size_t
74 smallest_unused_suffix(const std::string &prefix) const = 0;
75
82 virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const=0;
83};
84
91{
92public:
93 // constructors
94 explicit namespacet(const symbol_table_baset &_symbol_table)
95 { symbol_table1=&_symbol_table; symbol_table2=nullptr; }
96
98 const symbol_table_baset &_symbol_table1,
99 const symbol_table_baset &_symbol_table2)
100 {
101 symbol_table1=&_symbol_table1;
102 symbol_table2=&_symbol_table2;
103 }
104
106 const symbol_table_baset *_symbol_table1,
107 const symbol_table_baset *_symbol_table2)
108 {
109 symbol_table1=_symbol_table1;
110 symbol_table2=_symbol_table2;
111 }
112
114
117 bool lookup(const irep_idt &name, const symbolt *&symbol) const override;
118
120 std::size_t smallest_unused_suffix(const std::string &prefix) const override;
121
124 {
125 return *symbol_table1;
126 }
127
128protected:
130};
131
137{
138public:
139 // constructors
140 multi_namespacet():namespacet(nullptr, nullptr)
141 {
142 }
143
144 explicit multi_namespacet(const symbol_table_baset &symbol_table)
145 : namespacet(nullptr, nullptr)
146 {
147 add(symbol_table);
148 }
149
150 // these do the actual lookup
152
154 bool lookup(const irep_idt &name, const symbolt *&symbol) const override;
156 std::size_t smallest_unused_suffix(const std::string &prefix) const override;
157
162 void add(const symbol_table_baset &symbol_table)
163 {
164 symbol_table_list.push_back(&symbol_table);
165 }
166
167protected:
168 typedef std::vector<const symbol_table_baset *> symbol_table_listt;
170};
171
172#endif // CPROVER_UTIL_NAMESPACE_H
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:39
Base class for all expressions.
Definition expr.h:56
A multi namespace is essentially a namespace, with a list of namespaces.
Definition namespace.h:137
void add(const symbol_table_baset &symbol_table)
Add symbol table to the list of symbol tables this multi-namespace is working with.
Definition namespace.h:162
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
multi_namespacet(const symbol_table_baset &symbol_table)
Definition namespace.h:144
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
std::vector< const symbol_table_baset * > symbol_table_listt
Definition namespace.h:168
Basic interface for a namespace.
Definition namespace.h:34
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
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const =0
Searches for a symbol named name.
virtual std::size_t smallest_unused_suffix(const std::string &prefix) const =0
Returns the minimal integer n such that there is no symbol (in any of the symbol tables) whose name i...
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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().
namespacet(const symbol_table_baset &_symbol_table1, const symbol_table_baset &_symbol_table2)
Definition namespace.h:97
namespacet(const symbol_table_baset &_symbol_table)
Definition namespace.h:94
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition namespace.h:123
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().
namespacet(const symbol_table_baset *_symbol_table1, const symbol_table_baset *_symbol_table2)
Definition namespace.h:105
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:113
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
A tag-based type, i.e., typet with an identifier.
Definition std_types.h:396
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:199
The union type.
Definition c_types.h:147
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423