CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_scope.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_SCOPE_H
13#define CPROVER_CPP_CPP_SCOPE_H
14
15#include <iosfwd>
16#include <set>
17
18#include "cpp_id.h"
19
20class cpp_scopet:public cpp_idt
21{
22public:
24 {
25 is_scope=true;
26 }
27
28 typedef std::set<cpp_idt *> id_sett;
29
31
33 {
34 id_sett result;
35 lookup_rec(base_name_to_lookup, kind, result);
36 return result;
37 }
38
41 lookup_kindt kind,
43 {
44 id_sett result;
46 return result;
47 }
48
51
53 {
54 cpp_id_mapt::iterator it=
55 sub.insert(std::pair<irep_idt, cpp_idt>
56 (_base_name, cpp_idt()));
57
58 it->second.base_name=_base_name;
59 it->second.set_parent(*this);
60
61 return it->second;
62 }
63
65 {
66 cpp_id_mapt::iterator it=
67 sub.insert(std::pair<irep_idt, cpp_idt>
68 (cpp_id.base_name, cpp_id));
69
70 it->second.set_parent(*this);
71
72 return it->second;
73 }
74
76
77 bool is_root_scope() const
78 {
80 }
81
87
89 {
90 return static_cast<cpp_scopet &>(cpp_idt::get_parent());
91 }
92
94 {
95 cpp_scopet *p=this;
96
97 while(!p->is_global_scope())
98 p=&(p->get_parent());
99
100 return *p;
101 }
102
104 {
105 PRECONDITION(other.is_scope);
106 secondary_scopes.push_back(&other);
107 }
108
110 {
111 PRECONDITION(other.is_scope);
112 using_scopes.push_back(&other);
113 }
114
116
117protected:
118 void lookup_rec(const irep_idt &base_name, lookup_kindt kind, id_sett &);
119
120 void lookup_rec(
121 const irep_idt &base_name,
122 lookup_kindt kind,
124 id_sett &);
125};
126
128{
129public:
135};
136
137std::ostream &operator << (std::ostream &out, cpp_scopet::lookup_kindt);
138
139#endif // CPROVER_CPP_CPP_SCOPE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
irep_idt identifier
Definition cpp_id.h:72
scope_listt using_scopes
Definition cpp_id.h:108
cpp_idt & get_parent() const
Definition cpp_id.h:82
bool is_scope
Definition cpp_id.h:43
id_classt
Definition cpp_id.h:28
cpp_id_mapt sub
Definition cpp_id.h:104
id_classt id_class
Definition cpp_id.h:45
cpp_idt()
Definition cpp_id.cpp:18
void set_parent(cpp_idt &_parent)
Definition cpp_id.h:88
scope_listt secondary_scopes
Definition cpp_id.h:108
irep_idt base_name
Definition cpp_id.h:72
class cpp_scopet & new_scope(const irep_idt &new_scope_name)
cpp_scopet & get_parent() const
Definition cpp_scope.h:88
cpp_idt & insert(const irep_idt &_base_name)
Definition cpp_scope.h:52
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind, cpp_idt::id_classt identifier_class)
Definition cpp_scope.h:39
cpp_idt & insert(const cpp_idt &cpp_id)
Definition cpp_scope.h:64
cpp_scopet & get_global_scope()
Definition cpp_scope.h:93
bool is_global_scope() const
Definition cpp_scope.h:82
void add_using_scope(cpp_scopet &other)
Definition cpp_scope.h:109
id_sett lookup_identifier(const irep_idt &id, cpp_idt::id_classt identifier_class)
std::set< cpp_idt * > id_sett
Definition cpp_scope.h:28
void lookup_rec(const irep_idt &base_name, lookup_kindt kind, id_sett &)
Definition cpp_scope.cpp:27
id_sett lookup(const irep_idt &base_name_to_lookup, lookup_kindt kind)
Definition cpp_scope.h:32
bool is_root_scope() const
Definition cpp_scope.h:77
bool contains(const irep_idt &base_name_to_lookup)
void add_secondary_scope(cpp_scopet &other)
Definition cpp_scope.h:103
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
C++ Language Type Checking.
std::ostream & operator<<(std::ostream &out, cpp_scopet::lookup_kindt)
Definition cpp_scope.cpp:14
#define PRECONDITION(CONDITION)
Definition invariant.h:463