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
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
namespacet::symbol_table2
const symbol_table_baset * symbol_table2
Definition: namespace.h:130
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
c_enum_typet
The type of C enums.
Definition: std_types.h:619
typet
The type of an expression, extends irept.
Definition: type.h:28
invariant.h
namespace_baset
Basic interface for a namespace.
Definition: namespace.h:34
exprt
Base class for all expressions.
Definition: expr.h:52
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:489
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
namespacet::namespacet
namespacet(const symbol_table_baset &_symbol_table1, const symbol_table_baset &_symbol_table2)
Definition: namespace.h:98
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
union_tag_typet
A union tag type, i.e., union_typet with an identifier.
Definition: std_types.h:529
multi_namespacet::symbol_table_list
symbol_table_listt symbol_table_list
Definition: namespace.h:170
multi_namespacet::symbol_table_listt
std::vector< const symbol_table_baset * > symbol_table_listt
Definition: namespace.h:169
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
namespacet::namespacet
namespacet(const symbol_table_baset &_symbol_table)
Definition: namespace.h:95
namespace_baset::follow_macros
void follow_macros(exprt &) const
Follow macros to their values in a given expression.
Definition: namespace.cpp:99
multi_namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:191
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
namespace_baset::lookup
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:44
namespacet::smallest_unused_suffix
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:122
namespacet::namespacet
namespacet(const symbol_table_baset *_symbol_table1, const symbol_table_baset *_symbol_table2)
Definition: namespace.h:106
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
namespace_baset::~namespace_baset
virtual ~namespace_baset()
Definition: namespace.cpp:22
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:21
multi_namespacet::multi_namespacet
multi_namespacet()
Definition: namespace.h:141
namespacet::symbol_table1
const symbol_table_baset * symbol_table1
Definition: namespace.h:130
union_typet
The union type.
Definition: std_types.h:392
tag_typet
A tag-based type, i.e., typet with an identifier.
Definition: std_types.h:436
multi_namespacet::add
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
multi_namespacet::multi_namespacet
multi_namespacet(const symbol_table_baset &symbol_table)
Definition: namespace.h:145
namespacet::get_symbol_table
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:124
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
c_enum_tag_typet
C enum tag type, i.e., c_enum_typet with an identifier.
Definition: std_types.h:695
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:27
multi_namespacet
A multi namespace is essentially a namespace, with a list of namespaces.
Definition: namespace.h:137
multi_namespacet::smallest_unused_suffix
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:175
namespace_baset::smallest_unused_suffix
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...
validation_modet::INVARIANT
irep.h