cprover
cpp_scopes.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Type Checking
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CPP_CPP_SCOPES_H
13 #define CPROVER_CPP_CPP_SCOPES_H
14 
15 #include <set>
16 
17 #include <util/symbol.h>
18 #include <util/string_hash.h>
19 
20 #include "cpp_scope.h"
21 
23 {
24 public:
26  {
28  }
29 
30  typedef std::set<cpp_scopet *> scope_sett;
31  typedef std::set<cpp_idt *> id_sett;
32 
34  {
35  return *current_scope_ptr;
36  }
37 
39  const irep_idt &new_scope_name,
40  cpp_idt::id_classt id_class)
41  {
42  assert(!new_scope_name.empty());
43  cpp_scopet &n=current_scope_ptr->new_scope(new_scope_name);
44  n.id_class=id_class;
45  id_map[n.identifier]=&n;
47  return n;
48  }
49 
50  cpp_scopet &new_namespace(const irep_idt &new_scope_name)
51  {
52  return new_scope(new_scope_name, cpp_idt::id_classt::NAMESPACE);
53  }
54 
56 
58  const symbolt &symbol,
59  cpp_scopet &scope,
60  bool is_friend = false);
61 
62  cpp_idt &put_into_scope(const symbolt &symbol, bool is_friend = false)
63  {
64  return put_into_scope(symbol, current_scope(), is_friend);
65  }
66 
67  // mapping from function/class/scope names to their cpp_idt
68  typedef std::unordered_map<irep_idt, cpp_idt *> id_mapt;
70 
72 
73  cpp_idt &get_id(const irep_idt &identifier)
74  {
75  id_mapt::const_iterator it=id_map.find(identifier);
76  if(it==id_map.end())
77  throw "id '" + id2string(identifier) + "' not found";
78  return *(it->second);
79  }
80 
81  cpp_scopet &get_scope(const irep_idt &identifier)
82  {
83  cpp_idt &n=get_id(identifier);
84  assert(n.is_scope);
85  return (cpp_scopet &)n;
86  }
87 
88  cpp_scopet &set_scope(const irep_idt &identifier)
89  {
90  current_scope_ptr=&get_scope(identifier);
91  return current_scope();
92  }
93 
95  {
96  return root_scope;
97  }
98 
100  {
102  }
103 
104  void go_to(cpp_idt &id)
105  {
106  assert(id.is_scope);
107  current_scope_ptr=static_cast<cpp_scopet*>(&id);
108  }
109 
110  // move up to next global scope
112  {
114  }
115 
117  {
118  return current_scope().get_global_scope();
119  }
120 
121  void print_current(std::ostream &out) const;
122 
123 protected:
124  // the root scope
126 };
127 
129 {
130 public:
131  explicit cpp_save_scopet(cpp_scopest &_cpp_scopes):
132  cpp_scopes(_cpp_scopes),
133  saved_scope(_cpp_scopes.current_scope_ptr)
134  {
135  }
136 
138  {
139  restore();
140  }
141 
142  void restore()
143  {
145  }
146 
147 protected:
150 };
151 
152 #endif // CPROVER_CPP_CPP_SCOPES_H
cpp_scopet::new_scope
class cpp_scopet & new_scope(const irep_idt &new_scope_name)
Definition: cpp_scope.cpp:192
cpp_scopet::get_global_scope
cpp_scopet & get_global_scope()
Definition: cpp_scope.h:93
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
cpp_scope.h
C++ Language Type Checking.
cpp_scopet
Definition: cpp_scope.h:21
cpp_save_scopet::cpp_save_scopet
cpp_save_scopet(cpp_scopest &_cpp_scopes)
Definition: cpp_scopes.h:131
cpp_save_scopet
Definition: cpp_scopes.h:129
cpp_scopest::id_map
id_mapt id_map
Definition: cpp_scopes.h:69
cpp_scopest::new_namespace
cpp_scopet & new_namespace(const irep_idt &new_scope_name)
Definition: cpp_scopes.h:50
cpp_scopest::put_into_scope
cpp_idt & put_into_scope(const symbolt &symbol, bool is_friend=false)
Definition: cpp_scopes.h:62
cpp_idt::identifier
irep_idt identifier
Definition: cpp_id.h:78
cpp_scopest::get_scope
cpp_scopet & get_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:81
cpp_scopest::new_scope
cpp_scopet & new_scope(const irep_idt &new_scope_name, cpp_idt::id_classt id_class)
Definition: cpp_scopes.h:38
cpp_scopest::put_into_scope
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
Definition: cpp_scopes.cpp:22
cpp_save_scopet::saved_scope
cpp_scopet * saved_scope
Definition: cpp_scopes.h:149
cpp_idt
Definition: cpp_id.h:29
cpp_scopest::get_root_scope
cpp_scopet & get_root_scope()
Definition: cpp_scopes.h:94
cpp_idt::id_classt
id_classt
Definition: cpp_id.h:34
cpp_scopest::get_global_scope
cpp_scopet & get_global_scope()
Definition: cpp_scopes.h:116
cpp_save_scopet::cpp_scopes
cpp_scopest & cpp_scopes
Definition: cpp_scopes.h:148
cpp_idt::is_scope
bool is_scope
Definition: cpp_id.h:49
cpp_scopest::root_scope
cpp_root_scopet root_scope
Definition: cpp_scopes.h:125
cpp_scopest::go_to_global_scope
void go_to_global_scope()
Definition: cpp_scopes.h:111
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
cpp_scopest::current_scope
cpp_scopet & current_scope()
Definition: cpp_scopes.h:33
cpp_scopest::current_scope_ptr
cpp_scopet * current_scope_ptr
Definition: cpp_scopes.h:71
cpp_scopest::id_sett
std::set< cpp_idt * > id_sett
Definition: cpp_scopes.h:31
string_hash.h
string hashing
cpp_root_scopet
Definition: cpp_scope.h:128
symbol.h
Symbol table entry.
dstringt::empty
bool empty() const
Definition: dstring.h:88
cpp_scopest
Definition: cpp_scopes.h:23
cpp_scopest::go_to
void go_to(cpp_idt &id)
Definition: cpp_scopes.h:104
cpp_scopest::cpp_scopest
cpp_scopest()
Definition: cpp_scopes.h:25
cpp_scopest::go_to_root_scope
void go_to_root_scope()
Definition: cpp_scopes.h:99
cpp_scopest::new_block_scope
cpp_scopet & new_block_scope()
Definition: cpp_scopes.cpp:16
cpp_save_scopet::restore
void restore()
Definition: cpp_scopes.h:142
symbolt
Symbol table entry.
Definition: symbol.h:28
cpp_idt::id_class
id_classt id_class
Definition: cpp_id.h:51
cpp_save_scopet::~cpp_save_scopet
~cpp_save_scopet()
Definition: cpp_scopes.h:137
cpp_scopest::print_current
void print_current(std::ostream &out) const
Definition: cpp_scopes.cpp:71
cpp_scopest::id_mapt
std::unordered_map< irep_idt, cpp_idt * > id_mapt
Definition: cpp_scopes.h:68
cpp_scopest::get_id
cpp_idt & get_id(const irep_idt &identifier)
Definition: cpp_scopes.h:73
cpp_scopest::scope_sett
std::set< cpp_scopet * > scope_sett
Definition: cpp_scopes.h:30
cpp_idt::id_classt::NAMESPACE
@ NAMESPACE
cpp_scopest::set_scope
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:88