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 union_tag_typet;
20 class union_typet;
21 class struct_tag_typet;
22 class struct_typet;
23 class c_enum_typet;
24 class c_enum_tag_typet;
25 
27 {
28 public:
29  // service methods
30  const symbolt &lookup(const irep_idt &name) const
31  {
32  const symbolt *symbol;
33  if(lookup(name, symbol))
34  throw "identifier "+id2string(name)+" not found";
35  return *symbol;
36  }
37 
38  const symbolt &lookup(const irept &irep) const
39  {
40  return lookup(irep.get(ID_identifier));
41  }
42 
43  virtual ~namespace_baset();
44 
45  void follow_symbol(irept &irep) const;
46  void follow_macros(exprt &expr) const;
47  const typet &follow(const typet &src) const;
48 
49  // These produce union_typet, struct_typet, c_enum_typet or
50  // the incomplete version.
51  const typet &follow_tag(const union_tag_typet &src) const;
52  const typet &follow_tag(const struct_tag_typet &src) const;
53  const typet &follow_tag(const c_enum_tag_typet &src) const;
54 
55  // these do the actual lookup
56  virtual unsigned get_max(const std::string &prefix) const=0;
57  virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const=0;
58 };
59 
63 {
64 public:
65  // constructors
66  explicit namespacet(const symbol_tablet &_symbol_table)
67  { symbol_table1=&_symbol_table; symbol_table2=nullptr; }
68 
70  const symbol_tablet &_symbol_table1,
71  const symbol_tablet &_symbol_table2)
72  {
73  symbol_table1=&_symbol_table1;
74  symbol_table2=&_symbol_table2;
75  }
76 
78  const symbol_tablet *_symbol_table1,
79  const symbol_tablet *_symbol_table2)
80  {
81  symbol_table1=_symbol_table1;
82  symbol_table2=_symbol_table2;
83  }
84 
86 
87  // these do the actual lookup
88  virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const;
89  virtual unsigned get_max(const std::string &prefix) const;
90 
92  {
93  return *symbol_table1;
94  }
95 
96 protected:
97  const symbol_tablet *symbol_table1, *symbol_table2;
98 };
99 
101 {
102 public:
103  // constructors
104  multi_namespacet():namespacet(nullptr, nullptr)
105  {
106  }
107 
109  const symbol_tablet &symbol_table):namespacet(nullptr, nullptr)
110  {
111  add(symbol_table);
112  }
113 
114  // these do the actual lookup
116 
117  virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const;
118  virtual unsigned get_max(const std::string &prefix) const;
119 
120  void add(const symbol_tablet &symbol_table)
121  {
122  symbol_table_list.push_back(&symbol_table);
123  }
124 
125 protected:
126  typedef std::vector<const symbol_tablet *> symbol_table_listt;
127  symbol_table_listt symbol_table_list;
128 };
129 
130 #endif // CPROVER_UTIL_NAMESPACE_H
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
void add(const symbol_tablet &symbol_table)
Definition: namespace.h:120
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const symbol_tablet & get_symbol_table() const
Definition: namespace.h:91
symbol_table_listt symbol_table_list
Definition: namespace.h:127
A union tag type.
Definition: std_types.h:554
A struct tag type.
Definition: std_types.h:517
virtual unsigned get_max(const std::string &prefix) const =0
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
Structure type.
Definition: std_types.h:296
const symbolt & lookup(const irep_idt &name) const
Definition: namespace.h:30
virtual ~namespace_baset()
Definition: namespace.cpp:39
std::vector< const symbol_tablet * > symbol_table_listt
Definition: namespace.h:126
const typet & follow_tag(const union_tag_typet &src) const
Definition: namespace.cpp:83
void follow_macros(exprt &expr) const
Definition: namespace.cpp:107
namespacet(const symbol_tablet &_symbol_table1, const symbol_tablet &_symbol_table2)
Definition: namespace.h:69
The symbol table.
Definition: symbol_table.h:52
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:62
namespacet(const symbol_tablet &_symbol_table)
Definition: namespace.h:66
Base class for tree-like data structures with sharing.
Definition: irep.h:87
namespacet(const symbol_tablet *_symbol_table1, const symbol_tablet *_symbol_table2)
Definition: namespace.h:77
multi_namespacet(const symbol_tablet &symbol_table)
Definition: namespace.h:108
void follow_symbol(irept &irep) const
Definition: namespace.cpp:43
Base class for all expressions.
Definition: expr.h:46
The union type.
Definition: std_types.h:424
const symbol_tablet * symbol_table2
Definition: namespace.h:97
const symbolt & lookup(const irept &irep) const
Definition: namespace.h:38
The type of C enums.
Definition: std_types.h:637
An enum tag type.
Definition: std_types.h:698