CBMC
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 exprt;
17 class symbolt;
18 class typet;
19 class symbol_exprt;
20 class tag_typet;
21 class union_typet;
22 class struct_typet;
23 class c_enum_typet;
24 class union_tag_typet;
25 class struct_tag_typet;
26 class c_enum_tag_typet;
27 class symbol_table_baset;
28 
34 {
35 public:
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);
47  INVARIANT(
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 {
92 public:
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 
128 protected:
130 };
131 
137 {
138 public:
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 
167 protected:
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: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: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
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:43
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
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().
Definition: namespace.cpp:173
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 symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:43
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
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 symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:43
const symbol_table_baset * symbol_table1
Definition: namespace.h:129
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 * 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
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:123
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:177
The union type.
Definition: c_types.h:125
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47