CBMC
cpp_destructor.cpp
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 #include "cpp_typecheck.h"
13 
14 #include <util/arith_tools.h>
15 
16 #include <util/c_types.h>
17 
19 std::optional<codet> cpp_typecheckt::cpp_destructor(
20  const source_locationt &source_location,
21  const exprt &object)
22 {
23  elaborate_class_template(object.type());
24 
25  CHECK_RETURN(!is_reference(object.type()));
26 
27  // PODs don't need a destructor
28  if(cpp_is_pod(object.type()))
29  return {};
30 
31  if(object.type().id() == ID_array)
32  {
33  const exprt &size_expr = to_array_type(object.type()).size();
34 
35  if(size_expr.id() == ID_infinity)
36  return {}; // don't initialize
37 
38  exprt tmp_size=size_expr;
39  make_constant_index(tmp_size);
40 
41  mp_integer s;
42  if(to_integer(to_constant_expr(tmp_size), s))
43  {
44  error().source_location=source_location;
45  error() << "array size '" << to_string(size_expr) << "' is not a constant"
46  << eom;
47  throw 0;
48  }
49 
50  code_blockt new_code;
51  new_code.add_source_location()=source_location;
52 
53  // for each element of the array, call the destructor
54  for(mp_integer i=0; i < s; ++i)
55  {
56  exprt constant = from_integer(i, c_index_type());
57  constant.add_source_location()=source_location;
58 
59  index_exprt index(object, constant);
60  index.add_source_location()=source_location;
61 
62  auto i_code = cpp_destructor(source_location, index);
63  if(i_code.has_value())
64  new_code.add_to_operands(std::move(i_code.value()));
65  }
66 
67  return std::move(new_code);
68  }
69  else
70  {
71  const struct_typet &struct_type =
72  follow_tag(to_struct_tag_type(object.type()));
73 
74  // enter struct scope
75  cpp_save_scopet save_scope(cpp_scopes);
76  cpp_scopes.set_scope(struct_type.get(ID_name));
77 
78  // find name of destructor
79  const struct_typet::componentst &components=
80  struct_type.components();
81 
82  irep_idt dtor_name;
83 
84  for(const auto &c : components)
85  {
86  const typet &type = c.type();
87 
88  if(
89  !c.get_bool(ID_from_base) && type.id() == ID_code &&
90  to_code_type(type).return_type().id() == ID_destructor)
91  {
92  dtor_name = c.get_base_name();
93  break;
94  }
95  }
96 
97  INVARIANT(!dtor_name.empty(), "non-PODs should have a destructor");
98 
99  cpp_namet cpp_name(dtor_name, source_location);
100 
101  exprt member(ID_member);
102  member.add(ID_component_cpp_name) = cpp_name;
103  member.copy_to_operands(object);
104 
105  side_effect_expr_function_callt function_call(
106  std::move(member), {}, uninitialized_typet{}, source_location);
107 
110 
111  code_expressiont new_code(function_call);
112  new_code.add_source_location() = source_location;
113 
114  return std::move(new_code);
115  }
116 }
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.
Definition: arith_tools.cpp:20
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:840
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
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:87
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:16
void elaborate_class_template(const typet &type)
elaborate class template instances
std::optional< codet > cpp_destructor(const source_locationt &source_location, const exprt &object)
std::string to_string(const typet &) override
cpp_scopest cpp_scopes
Definition: cpp_typecheck.h:92
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
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:163
source_locationt & add_source_location()
Definition: expr.h:236
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:170
Array index operator.
Definition: std_expr.h:1465
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
const irep_idt & id() const
Definition: irep.h:388
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
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
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.
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:145
BigInt mp_integer
Definition: smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3045
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:788
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518