CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_scopes.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C++ Language Type Checking
4
5Author: 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 "cpp_scope.h"
18
19class symbolt;
20
22{
23public:
28
29 typedef std::set<cpp_scopet *> scope_sett;
30 typedef std::set<cpp_idt *> id_sett;
31
33 {
34 return *current_scope_ptr;
35 }
36
39 cpp_idt::id_classt id_class)
40 {
43 n.id_class=id_class;
44 id_map[n.identifier]=&n;
46 return n;
47 }
48
53
55
57 const symbolt &symbol,
58 cpp_scopet &scope,
59 bool is_friend = false);
60
61 cpp_idt &put_into_scope(const symbolt &symbol, bool is_friend = false)
62 {
63 return put_into_scope(symbol, current_scope(), is_friend);
64 }
65
66 // mapping from function/class/scope names to their cpp_idt
67 typedef std::unordered_map<irep_idt, cpp_idt *> id_mapt;
69
71
72 cpp_idt &get_id(const irep_idt &identifier)
73 {
74 id_mapt::const_iterator it=id_map.find(identifier);
75 if(it==id_map.end())
76 throw "id '" + id2string(identifier) + "' not found";
77 return *(it->second);
78 }
79
80 cpp_scopet &get_scope(const irep_idt &identifier)
81 {
82 cpp_idt &n=get_id(identifier);
83 CHECK_RETURN(n.is_scope);
84 return (cpp_scopet &)n;
85 }
86
87 cpp_scopet &set_scope(const irep_idt &identifier)
88 {
89 current_scope_ptr=&get_scope(identifier);
90 return current_scope();
91 }
92
94 {
95 return root_scope;
96 }
97
102
103 void go_to(cpp_idt &id)
104 {
105 PRECONDITION(id.is_scope);
106 current_scope_ptr=static_cast<cpp_scopet*>(&id);
107 }
108
109 // move up to next global scope
114
119
120 void print_current(std::ostream &out) const;
121
122protected:
123 // the root scope
125};
126
128{
129public:
132 saved_scope(_cpp_scopes.current_scope_ptr)
133 {
134 }
135
137 {
138 restore();
139 }
140
145
146protected:
149};
150
151#endif // CPROVER_CPP_CPP_SCOPES_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
id_classt
Definition cpp_id.h:28
cpp_scopet * saved_scope
Definition cpp_scopes.h:148
cpp_scopest & cpp_scopes
Definition cpp_scopes.h:147
cpp_save_scopet(cpp_scopest &_cpp_scopes)
Definition cpp_scopes.h:130
void go_to_root_scope()
Definition cpp_scopes.h:98
void go_to(cpp_idt &id)
Definition cpp_scopes.h:103
void print_current(std::ostream &out) const
cpp_idt & get_id(const irep_idt &identifier)
Definition cpp_scopes.h:72
cpp_scopet & new_block_scope()
cpp_scopet * current_scope_ptr
Definition cpp_scopes.h:70
std::unordered_map< irep_idt, cpp_idt * > id_mapt
Definition cpp_scopes.h:67
std::set< cpp_scopet * > scope_sett
Definition cpp_scopes.h:29
std::set< cpp_idt * > id_sett
Definition cpp_scopes.h:30
cpp_idt & put_into_scope(const symbolt &symbol, cpp_scopet &scope, bool is_friend=false)
cpp_scopet & new_scope(const irep_idt &new_scope_name, cpp_idt::id_classt id_class)
Definition cpp_scopes.h:37
cpp_scopet & new_namespace(const irep_idt &new_scope_name)
Definition cpp_scopes.h:49
id_mapt id_map
Definition cpp_scopes.h:68
cpp_idt & put_into_scope(const symbolt &symbol, bool is_friend=false)
Definition cpp_scopes.h:61
cpp_scopet & get_global_scope()
Definition cpp_scopes.h:115
cpp_scopet & get_scope(const irep_idt &identifier)
Definition cpp_scopes.h:80
cpp_scopet & set_scope(const irep_idt &identifier)
Definition cpp_scopes.h:87
cpp_root_scopet root_scope
Definition cpp_scopes.h:124
void go_to_global_scope()
Definition cpp_scopes.h:110
cpp_scopet & current_scope()
Definition cpp_scopes.h:32
cpp_scopet & get_root_scope()
Definition cpp_scopes.h:93
class cpp_scopet & new_scope(const irep_idt &new_scope_name)
cpp_scopet & get_global_scope()
Definition cpp_scope.h:93
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Symbol table entry.
Definition symbol.h:28
C++ Language Type Checking.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define PRECONDITION(CONDITION)
Definition invariant.h:463