cprover
namespace.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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 
16 class symbol_tablet;
17 class exprt;
18 class symbolt;
19 class typet;
20 class symbol_exprt;
21 class tag_typet;
22 class union_typet;
23 class struct_typet;
24 class c_enum_typet;
25 class union_tag_typet;
26 class struct_tag_typet;
27 class c_enum_tag_typet;
28 class symbol_table_baset;
29 
35 {
36 public:
37  // service methods
38 
44  const symbolt &lookup(const irep_idt &name) const
45  {
46  const symbolt *symbol;
47  bool not_found = lookup(name, symbol);
48  INVARIANT(
49  !not_found,
50  "we are assuming that a name exists in the namespace "
51  "when this function is called - identifier " +
52  id2string(name) + " was not found");
53  return *symbol;
54  }
55 
56  const symbolt &lookup(const symbol_exprt &) const;
57  const symbolt &lookup(const tag_typet &) const;
58 
59  virtual ~namespace_baset();
60 
61  void follow_macros(exprt &) const;
62  const typet &follow(const typet &) const;
63 
64  // These produce union_typet, struct_typet, c_enum_typet or
65  // the incomplete version.
66  const union_typet &follow_tag(const union_tag_typet &) const;
67  const struct_typet &follow_tag(const struct_tag_typet &) const;
68  const c_enum_typet &follow_tag(const c_enum_tag_typet &) const;
69 
74  virtual std::size_t
75  smallest_unused_suffix(const std::string &prefix) const = 0;
76 
83  virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const=0;
84 };
85 
92 {
93 public:
94  // constructors
95  explicit namespacet(const symbol_table_baset &_symbol_table)
96  { symbol_table1=&_symbol_table; symbol_table2=nullptr; }
97 
99  const symbol_table_baset &_symbol_table1,
100  const symbol_table_baset &_symbol_table2)
101  {
102  symbol_table1=&_symbol_table1;
103  symbol_table2=&_symbol_table2;
104  }
105 
107  const symbol_table_baset *_symbol_table1,
108  const symbol_table_baset *_symbol_table2)
109  {
110  symbol_table1=_symbol_table1;
111  symbol_table2=_symbol_table2;
112  }
113 
115 
118  bool lookup(const irep_idt &name, const symbolt *&symbol) const override;
119 
121  std::size_t smallest_unused_suffix(const std::string &prefix) const override;
122 
125  {
126  return *symbol_table1;
127  }
128 
129 protected:
131 };
132 
138 {
139 public:
140  // constructors
141  multi_namespacet():namespacet(nullptr, nullptr)
142  {
143  }
144 
145  explicit multi_namespacet(const symbol_table_baset &symbol_table)
146  : namespacet(nullptr, nullptr)
147  {
148  add(symbol_table);
149  }
150 
151  // these do the actual lookup
153 
155  bool lookup(const irep_idt &name, const symbolt *&symbol) const override;
157  std::size_t smallest_unused_suffix(const std::string &prefix) const override;
158 
163  void add(const symbol_table_baset &symbol_table)
164  {
165  symbol_table_list.push_back(&symbol_table);
166  }
167 
168 protected:
169  typedef std::vector<const symbol_table_baset *> symbol_table_listt;
171 };
172 
173 #endif // CPROVER_UTIL_NAMESPACE_H
The type of an expression, extends irept.
Definition: type.h:28
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:436
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symbol_table_listt symbol_table_list
Definition: namespace.h:170
const symbol_table_baset * symbol_table2
Definition: namespace.h:130
A union tag type, i.e., union_typet with an identifier.
Definition: std_types.h:529
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:489
Symbol table entry.
Definition: symbol.h:27
Structure type, corresponds to C style structs.
Definition: std_types.h:225
std::vector< const symbol_table_baset * > symbol_table_listt
Definition: namespace.h:169
namespacet(const symbol_table_baset &_symbol_table)
Definition: namespace.h:95
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
virtual ~namespace_baset()
Definition: namespace.cpp:22
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
Definition: namespace.cpp:99
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:175
namespacet(const symbol_table_baset &_symbol_table1, const symbol_table_baset &_symbol_table2)
Definition: namespace.h:98
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:124
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
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:163
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:36
multi_namespacet(const symbol_table_baset &symbol_table)
Definition: namespace.h:145
const symbol_table_baset * symbol_table1
Definition: namespace.h:130
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
A multi namespace is essentially a namespace, with a list of namespaces.
Definition: namespace.h:137
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:191
Base class for all expressions.
Definition: expr.h:52
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:122
The union type.
Definition: std_types.h:392
The symbol table base class interface.
namespacet(const symbol_table_baset *_symbol_table1, const symbol_table_baset *_symbol_table2)
Definition: namespace.h:106
Basic interface for a namespace.
Definition: namespace.h:34
Expression to hold a symbol (variable)
Definition: std_expr.h:88
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...
The type of C enums.
Definition: std_types.h:619
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:695
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140