cprover
Loading...
Searching...
No Matches
cpp_destructor.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 <util/arith_tools.h>
15
16#include <util/c_types.h>
17
20 const source_locationt &source_location,
21 const exprt &object)
22{
23 elaborate_class_template(object.type());
24
25 typet tmp_type(follow(object.type()));
26 CHECK_RETURN(!is_reference(tmp_type));
27
28 // PODs don't need a destructor
29 if(cpp_is_pod(tmp_type))
30 return {};
31
32 if(tmp_type.id()==ID_array)
33 {
34 const exprt &size_expr=
35 to_array_type(tmp_type).size();
36
37 if(size_expr.id() == ID_infinity)
38 return {}; // don't initialize
39
40 exprt tmp_size=size_expr;
41 make_constant_index(tmp_size);
42
43 mp_integer s;
44 if(to_integer(to_constant_expr(tmp_size), s))
45 {
46 error().source_location=source_location;
47 error() << "array size '" << to_string(size_expr) << "' is not a constant"
48 << eom;
49 throw 0;
50 }
51
52 code_blockt new_code;
53 new_code.add_source_location()=source_location;
54
55 // for each element of the array, call the destructor
56 for(mp_integer i=0; i < s; ++i)
57 {
58 exprt constant = from_integer(i, c_index_type());
59 constant.add_source_location()=source_location;
60
61 index_exprt index(object, constant);
62 index.add_source_location()=source_location;
63
64 auto i_code = cpp_destructor(source_location, index);
65 if(i_code.has_value())
66 new_code.add_to_operands(std::move(i_code.value()));
67 }
68
69 return std::move(new_code);
70 }
71 else
72 {
73 const struct_typet &struct_type=
74 to_struct_type(tmp_type);
75
76 // enter struct scope
77 cpp_save_scopet save_scope(cpp_scopes);
78 cpp_scopes.set_scope(struct_type.get(ID_name));
79
80 // find name of destructor
81 const struct_typet::componentst &components=
82 struct_type.components();
83
84 irep_idt dtor_name;
85
86 for(const auto &c : components)
87 {
88 const typet &type = c.type();
89
90 if(
91 !c.get_bool(ID_from_base) && type.id() == ID_code &&
92 to_code_type(type).return_type().id() == ID_destructor)
93 {
94 dtor_name = c.get_base_name();
95 break;
96 }
97 }
98
99 INVARIANT(!dtor_name.empty(), "non-PODs should have a destructor");
100
101 cpp_namet cpp_name(dtor_name, source_location);
102
103 exprt member(ID_member);
104 member.add(ID_component_cpp_name) = cpp_name;
105 member.copy_to_operands(object);
106
108 std::move(member), {}, uninitialized_typet{}, source_location);
109
112
113 code_expressiont new_code(function_call);
114 new_code.add_source_location() = source_location;
115
116 return std::move(new_code);
117 }
118}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool to_integer(const constant_exprt &expr, mp_integer &int_value)
Convert a constant expression expr to an arbitrary-precision integer.
bitvector_typet c_index_type()
Definition c_types.cpp:16
static void make_already_typechecked(exprt &expr)
const exprt & size() const
Definition std_types.h:796
virtual void make_constant_index(exprt &expr)
A codet representing sequential composition of program statements.
Definition std_code.h:130
codet representation of an expression statement.
Definition std_code.h:1394
const typet & return_type() const
Definition std_types.h:645
cpp_scopet & set_scope(const irep_idt &identifier)
Definition cpp_scopes.h:87
optionalt< codet > cpp_destructor(const source_locationt &source_location, const exprt &object)
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
bool cpp_is_pod(const typet &type) const
void elaborate_class_template(const typet &type)
elaborate class template instances
std::string to_string(const typet &) override
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:39
bool empty() const
Definition dstring.h:90
Base class for all expressions.
Definition expr.h:56
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition expr.h:155
source_locationt & add_source_location()
Definition expr.h:228
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition expr.h:162
Array index operator.
Definition std_expr.h:1410
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:396
irept & add(const irep_idt &name)
Definition irep.cpp:111
source_locationt source_location
Definition message.h:247
mstreamt & error() const
Definition message.h:399
static eomt eom
Definition message.h:297
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
A side_effect_exprt representation of a function call side effect.
Definition std_code.h:1692
Structure type, corresponds to C style structs.
Definition std_types.h:231
const componentst & components() const
Definition std_types.h:147
std::vector< componentt > componentst
Definition std_types.h:140
The type of an expression, extends irept.
Definition type.h:29
C++ Language Type Checking.
nonstd::optional< T > optionalt
Definition optional.h:35
bool is_reference(const typet &type)
Returns true if the type is a reference.
BigInt mp_integer
Definition smt_terms.h:18
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844