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 symbol_typet;
22 class tag_typet;
23 class union_typet;
24 class struct_typet;
25 class c_enum_typet;
26 class union_tag_typet;
27 class struct_tag_typet;
28 class c_enum_tag_typet;
29 class symbol_table_baset;
30 
36 {
37 public:
38  // service methods
39 
45  const symbolt &lookup(const irep_idt &name) const
46  {
47  const symbolt *symbol;
48  bool not_found = lookup(name, symbol);
49  INVARIANT(
50  !not_found,
51  "we are assuming that a name exists in the namespace "
52  "when this function is called - identifier " +
53  id2string(name) + " was not found");
54  return *symbol;
55  }
56 
57  const symbolt &lookup(const symbol_exprt &) const;
58  const symbolt &lookup(const symbol_typet &) const;
59  const symbolt &lookup(const tag_typet &) const;
60 
61  virtual ~namespace_baset();
62 
63  void follow_macros(exprt &) const;
64  const typet &follow(const typet &) const;
65 
66  // These produce union_typet, struct_typet, c_enum_typet or
67  // the incomplete version.
68  const union_typet &follow_tag(const union_tag_typet &) const;
69  const struct_typet &follow_tag(const struct_tag_typet &) const;
70  const c_enum_typet &follow_tag(const c_enum_tag_typet &) const;
71 
76  virtual std::size_t
77  smallest_unused_suffix(const std::string &prefix) const = 0;
78 
85  virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const=0;
86 };
87 
94 {
95 public:
96  // constructors
97  explicit namespacet(const symbol_table_baset &_symbol_table)
98  { symbol_table1=&_symbol_table; symbol_table2=nullptr; }
99 
101  const symbol_table_baset &_symbol_table1,
102  const symbol_table_baset &_symbol_table2)
103  {
104  symbol_table1=&_symbol_table1;
105  symbol_table2=&_symbol_table2;
106  }
107 
109  const symbol_table_baset *_symbol_table1,
110  const symbol_table_baset *_symbol_table2)
111  {
112  symbol_table1=_symbol_table1;
113  symbol_table2=_symbol_table2;
114  }
115 
117 
120  bool lookup(const irep_idt &name, const symbolt *&symbol) const override;
121 
123  std::size_t smallest_unused_suffix(const std::string &prefix) const override;
124 
127  {
128  return *symbol_table1;
129  }
130 
131 protected:
133 };
134 
140 {
141 public:
142  // constructors
143  multi_namespacet():namespacet(nullptr, nullptr)
144  {
145  }
146 
147  explicit multi_namespacet(const symbol_table_baset &symbol_table)
148  : namespacet(nullptr, nullptr)
149  {
150  add(symbol_table);
151  }
152 
153  // these do the actual lookup
155 
157  bool lookup(const irep_idt &name, const symbolt *&symbol) const override;
159  std::size_t smallest_unused_suffix(const std::string &prefix) const override;
160 
165  void add(const symbol_table_baset &symbol_table)
166  {
167  symbol_table_list.push_back(&symbol_table);
168  }
169 
170 protected:
171  typedef std::vector<const symbol_table_baset *> symbol_table_listt;
173 };
174 
175 #endif // CPROVER_UTIL_NAMESPACE_H
The type of an expression, extends irept.
Definition: type.h:27
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:476
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symbol_table_listt symbol_table_list
Definition: namespace.h:172
const symbol_table_baset * symbol_table2
Definition: namespace.h:132
A union tag type, i.e., union_typet with an identifier.
Definition: std_types.h:569
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:529
Symbol table entry.
Definition: symbol.h:27
Structure type, corresponds to C style structs.
Definition: std_types.h:288
std::vector< const symbol_table_baset * > symbol_table_listt
Definition: namespace.h:171
namespacet(const symbol_table_baset &_symbol_table)
Definition: namespace.h:97
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:45
virtual ~namespace_baset()
Definition: namespace.cpp:22
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
Definition: namespace.cpp:124
A reference into the symbol table.
Definition: std_types.h:62
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:200
namespacet(const symbol_table_baset &_symbol_table1, const symbol_table_baset &_symbol_table2)
Definition: namespace.h:100
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:126
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:93
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:165
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
multi_namespacet(const symbol_table_baset &symbol_table)
Definition: namespace.h:147
const symbol_table_baset * symbol_table1
Definition: namespace.h:132
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
A multi namespace is essentially a namespace, with a list of namespaces.
Definition: namespace.h:139
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:216
Base class for all expressions.
Definition: expr.h:54
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:147
The union type.
Definition: std_types.h:437
The symbol table base class interface.
namespacet(const symbol_table_baset *_symbol_table1, const symbol_table_baset *_symbol_table2)
Definition: namespace.h:108
Basic interface for a namespace.
Definition: namespace.h:35
Expression to hold a symbol (variable)
Definition: std_expr.h:154
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:659
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:735
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:165