CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cpp_typecheck_bases.cpp
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#include "cpp_typecheck.h"
13
14#include <set>
15
16#include "cpp_typecheck_fargs.h"
17
19{
20 std::set<irep_idt> bases;
21 std::set<irep_idt> vbases;
22
24
26
27 for(auto &base : bases_irep)
28 {
29 const cpp_namet &name = to_cpp_name(base.find(ID_name));
30
32 resolve(
33 name,
36
38 {
40 error() << "expected type as struct/class base" << eom;
41 throw 0;
42 }
43
44 // elaborate any class template instances given as bases
46
47 if(base_symbol_expr.type().id() != ID_struct_tag)
48 {
50 error() << "expected type symbol as struct/class base" << eom;
51 throw 0;
52 }
53
54 const symbolt &base_symbol =
56
57 if(base_symbol.type.id() != ID_struct)
58 {
60 error() << "expected struct or class as base, but got '"
61 << to_string(base_symbol.type) << "'" << eom;
62 throw 0;
63 }
64
65 if(to_struct_type(base_symbol.type).is_incomplete())
66 {
68 error() << "base type is incomplete" << eom;
69 throw 0;
70 }
71
72 bool virtual_base = base.get_bool(ID_virtual);
74
75 if(class_access.empty())
77
80
81 if(virtual_base)
83
84 base.swap(base_symbol_expr);
85
86 // Add base scopes as parents to the current scope
88 static_cast<cpp_scopet &>(*cpp_scopes.id_map[base_symbol.name]));
89
92
96 type,
97 bases,
98 vbases,
100 }
101
102 if(!vbases.empty())
103 {
104 // add a flag to determine
105 // if this is the most-derived-object
107 cpp_scopes.current_scope().prefix + "::" + "@most_derived", bool_typet());
108
109 most_derived.set_access(ID_public);
110 most_derived.set_base_name("@most_derived");
111 most_derived.set_pretty_name("@most_derived");
112 most_derived.add_source_location()=type.source_location();
114
115 to_struct_type(type).components().push_back(most_derived);
116 }
117}
118
120 const struct_typet &from,
121 const irep_idt &access,
123 std::set<irep_idt> &bases,
124 std::set<irep_idt> &vbases,
125 bool is_virtual)
126{
127 const irep_idt &from_name = from.get(ID_name);
128
129 if(is_virtual && vbases.find(from_name)!=vbases.end())
130 return;
131
132 if(bases.find(from_name)!=bases.end())
133 {
134 error().source_location=to.source_location();
135 error() << "non-virtual base class " << from_name
136 << " inherited multiple times" << eom;
137 throw 0;
138 }
139
140 bases.insert(from_name);
141
142 if(is_virtual)
143 vbases.insert(from_name);
144
145 // look at the the parents of the base type
146 for(const auto &b : from.bases())
147 {
149
150 if(access==ID_private)
154
155 const symbolt &symb = lookup(b.type());
156
157 const bool is_virtual_base = b.get_bool(ID_virtual);
158
159 // recursive call
161 to_struct_type(symb.type),
163 to,
164 bases,
165 vbases,
167 }
168
169 // add the components
170 struct_typet::componentst &dest_c=to.components();
171
172 for(const auto &c : from.components())
173 {
174 if(c.get_bool(ID_from_base))
175 continue;
176
177 // copy the component
178 dest_c.push_back(c);
179
180 // now twiddle the copy
182 component.set(ID_from_base, true);
183
184 irep_idt comp_access=component.get_access();
185
186 if(access==ID_public)
187 {
189 component.set_access(ID_noaccess);
190 }
191 else if(access == ID_protected)
192 {
194 component.set_access(ID_noaccess);
195 else
196 component.set_access(ID_private);
197 }
198 else if(access == ID_private)
199 {
201 component.set_access(ID_noaccess);
202 else
203 component.set_access(ID_private);
204 }
205 else
207
208 // put into scope
209 }
210}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
The Boolean type.
Definition std_types.h:36
std::string prefix
Definition cpp_id.h:79
const source_locationt & source_location() const
Definition cpp_name.h:73
id_mapt id_map
Definition cpp_scopes.h:68
cpp_scopet & current_scope()
Definition cpp_scopes.h:32
void add_secondary_scope(cpp_scopet &other)
Definition cpp_scope.h:103
void put_compound_into_scope(const struct_union_typet::componentt &component)
void add_base_components(const struct_typet &from, const irep_idt &access, struct_typet &to, std::set< irep_idt > &bases, std::set< irep_idt > &vbases, bool is_virtual)
void typecheck_compound_bases(struct_typet &type)
void elaborate_class_template(const typet &type)
elaborate class template instances
std::string to_string(const typet &) override
exprt resolve(const cpp_namet &cpp_name, const cpp_typecheck_resolvet::wantt want, const cpp_typecheck_fargst &fargs, bool fail_with_exception=true)
cpp_scopest cpp_scopes
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
subt & get_sub()
Definition irep.h:448
irept & add(const irep_idt &name)
Definition irep.cpp:103
source_locationt source_location
Definition message.h:239
mstreamt & error() const
Definition message.h:391
static eomt eom
Definition message.h:289
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Structure type, corresponds to C style structs.
Definition std_types.h:231
irep_idt default_access() const
Return the access specification for members where access has not been modified.
Definition std_types.h:179
std::vector< componentt > componentst
Definition std_types.h:140
Symbol table entry.
Definition symbol.h:28
const source_locationt & source_location() const
Definition type.h:72
cpp_namet & to_cpp_name(irept &cpp_name)
Definition cpp_name.h:148
C++ Language Type Checking.
C++ Language Type Checking.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition std_expr.cpp:97
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:518