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 "deprecate.h"
14 #include "invariant.h"
15 #include "irep.h"
16 
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 struct_union_typet;
25 class c_enum_typet;
26 class union_tag_typet;
27 class struct_tag_typet;
29 class c_enum_tag_typet;
30 class symbol_table_baset;
31 
37 {
38 public:
39  // service methods
40 
46  const symbolt &lookup(const irep_idt &name) const
47  {
48  const symbolt *symbol;
49  bool not_found = lookup(name, symbol);
50  INVARIANT(
51  !not_found,
52  "we are assuming that a name exists in the namespace "
53  "when this function is called - identifier " +
54  id2string(name) + " was not found");
55  return *symbol;
56  }
57 
58  const symbolt &lookup(const symbol_exprt &) const;
59  const symbolt &lookup(const tag_typet &) const;
60 
61  virtual ~namespace_baset();
62 
63  void follow_macros(exprt &) const;
64  DEPRECATED(SINCE(2024, 2, 19, "use follow_tag(...) instead"))
65  const typet &follow(const typet &) const;
66 
67  const union_typet &follow_tag(const union_tag_typet &) const;
68  const struct_typet &follow_tag(const struct_tag_typet &) const;
69  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:
132  const symbol_table_baset *symbol_table1, *symbol_table2;
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
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:38
Base class for all expressions.
Definition: expr.h:56
A multi namespace is essentially a namespace, with a list of namespaces.
Definition: namespace.h:140
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
multi_namespacet(const symbol_table_baset &symbol_table)
Definition: namespace.h:147
symbol_table_listt symbol_table_list
Definition: namespace.h:172
std::vector< const symbol_table_baset * > symbol_table_listt
Definition: namespace.h:171
Basic interface for a namespace.
Definition: namespace.h:37
const symbolt & lookup(const irep_idt &name) const
Lookup a symbol in the namespace.
Definition: namespace.h:46
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:107
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:94
const symbol_table_baset * symbol_table1
Definition: namespace.h:132
namespacet(const symbol_table_baset &_symbol_table1, const symbol_table_baset &_symbol_table2)
Definition: namespace.h:100
namespacet(const symbol_table_baset &_symbol_table)
Definition: namespace.h:97
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:126
namespacet(const symbol_table_baset *_symbol_table1, const symbol_table_baset *_symbol_table2)
Definition: namespace.h:108
A struct or union tag type.
Definition: std_types.h:451
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:493
Structure type, corresponds to C style structs.
Definition: std_types.h:231
Base type for structs and unions.
Definition: std_types.h:62
Expression to hold a symbol (variable)
Definition: std_expr.h:131
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
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
#define DEPRECATED(msg)
Definition: deprecate.h:23
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40