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 "irep.h"
14 
15 class symbol_tablet;
16 class exprt;
17 class symbolt;
18 class typet;
19 class symbol_exprt;
20 class symbol_typet;
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 
30 {
31 public:
32  // service methods
33  const symbolt &lookup(const irep_idt &name) const
34  {
35  const symbolt *symbol;
36  if(lookup(name, symbol))
37  throw "identifier "+id2string(name)+" not found";
38  return *symbol;
39  }
40 
41  const symbolt &lookup(const symbol_exprt &) const;
42  const symbolt &lookup(const symbol_typet &) const;
43  const symbolt &lookup(const tag_typet &) const;
44 
45  virtual ~namespace_baset();
46 
47  void follow_macros(exprt &) const;
48  const typet &follow(const typet &) const;
49 
50  // These produce union_typet, struct_typet, c_enum_typet or
51  // the incomplete version.
52  const typet &follow_tag(const union_tag_typet &) const;
53  const typet &follow_tag(const struct_tag_typet &) const;
54  const typet &follow_tag(const c_enum_tag_typet &) const;
55 
60  virtual std::size_t
61  smallest_unused_suffix(const std::string &prefix) const = 0;
62 
69  virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const=0;
70 };
71 
75 {
76 public:
77  // constructors
78  explicit namespacet(const symbol_tablet &_symbol_table)
79  { symbol_table1=&_symbol_table; symbol_table2=nullptr; }
80 
82  const symbol_tablet &_symbol_table1,
83  const symbol_tablet &_symbol_table2)
84  {
85  symbol_table1=&_symbol_table1;
86  symbol_table2=&_symbol_table2;
87  }
88 
90  const symbol_tablet *_symbol_table1,
91  const symbol_tablet *_symbol_table2)
92  {
93  symbol_table1=_symbol_table1;
94  symbol_table2=_symbol_table2;
95  }
96 
98 
101  bool lookup(const irep_idt &name, const symbolt *&symbol) const override;
102 
104  std::size_t smallest_unused_suffix(const std::string &prefix) const override;
105 
107  {
108  return *symbol_table1;
109  }
110 
111 protected:
113 };
114 
116 {
117 public:
118  // constructors
119  multi_namespacet():namespacet(nullptr, nullptr)
120  {
121  }
122 
124  const symbol_tablet &symbol_table):namespacet(nullptr, nullptr)
125  {
126  add(symbol_table);
127  }
128 
129  // these do the actual lookup
131 
132  bool lookup(const irep_idt &name, const symbolt *&symbol) const override;
133  std::size_t smallest_unused_suffix(const std::string &prefix) const override;
134 
135  void add(const symbol_tablet &symbol_table)
136  {
137  symbol_table_list.push_back(&symbol_table);
138  }
139 
140 protected:
141  typedef std::vector<const symbol_tablet *> symbol_table_listt;
143 };
144 
145 #endif // CPROVER_UTIL_NAMESPACE_H
The type of an expression.
Definition: type.h:22
A generic tag-based type.
Definition: std_types.h:494
void add(const symbol_tablet &symbol_table)
Definition: namespace.h:135
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
const symbol_tablet & get_symbol_table() const
Definition: namespace.h:106
symbol_table_listt symbol_table_list
Definition: namespace.h:142
A union tag type.
Definition: std_types.h:584
A struct tag type.
Definition: std_types.h:547
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
Structure type.
Definition: std_types.h:297
const typet & follow_tag(const union_tag_typet &) const
Definition: namespace.cpp:74
const symbolt & lookup(const irep_idt &name) const
Definition: namespace.h:33
virtual ~namespace_baset()
Definition: namespace.cpp:36
std::vector< const symbol_tablet * > symbol_table_listt
Definition: namespace.h:141
void follow_macros(exprt &) const
Definition: namespace.cpp:98
A reference into the symbol table.
Definition: std_types.h:110
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:162
namespacet(const symbol_tablet &_symbol_table1, const symbol_tablet &_symbol_table2)
Definition: namespace.h:81
const symbol_tablet * symbol_table1
Definition: namespace.h:112
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
namespacet(const symbol_tablet &_symbol_table)
Definition: namespace.h:78
const typet & follow(const typet &) const
Definition: namespace.cpp:55
namespacet(const symbol_tablet *_symbol_table1, const symbol_tablet *_symbol_table2)
Definition: namespace.h:89
multi_namespacet(const symbol_tablet &symbol_table)
Definition: namespace.h:123
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:172
Base class for all expressions.
Definition: expr.h:42
std::size_t smallest_unused_suffix(const std::string &prefix) const override
See documentation for namespace_baset::smallest_unused_suffix().
Definition: namespace.cpp:117
The union type.
Definition: std_types.h:458
const symbol_tablet * symbol_table2
Definition: namespace.h:112
Expression to hold a symbol (variable)
Definition: std_expr.h:90
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:667
An enum tag type.
Definition: std_types.h:728
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130