cprover
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 
20  const source_locationt &source_location,
21  const exprt &object)
22 {
23  codet new_code;
24  new_code.add_source_location()=source_location;
25 
26  elaborate_class_template(object.type());
27 
28  typet tmp_type(follow(object.type()));
29 
30  assert(!is_reference(tmp_type));
31 
32  // PODs don't need a destructor
33  if(cpp_is_pod(tmp_type))
34  return {};
35 
36  if(tmp_type.id()==ID_array)
37  {
38  const exprt &size_expr=
39  to_array_type(tmp_type).size();
40 
41  if(size_expr.id() == ID_infinity)
42  return {}; // don't initialize
43 
44  exprt tmp_size=size_expr;
45  make_constant_index(tmp_size);
46 
47  mp_integer s;
48  if(to_integer(tmp_size, s))
49  {
50  error().source_location=source_location;
51  error() << "array size `" << to_string(size_expr)
52  << "' is not a constant" << eom;
53  throw 0;
54  }
55 
56  new_code.type().id(ID_code);
57  new_code.add_source_location()=source_location;
58  new_code.set_statement(ID_block);
59 
60  // for each element of the array, call the destructor
61  for(mp_integer i=0; i < s; ++i)
62  {
63  exprt constant=from_integer(i, index_type());
64  constant.add_source_location()=source_location;
65 
66  index_exprt index(object, constant);
67  index.add_source_location()=source_location;
68 
69  auto i_code = cpp_destructor(source_location, index);
70  if(i_code.has_value())
71  new_code.move_to_operands(i_code.value());
72  }
73  }
74  else
75  {
76  const struct_typet &struct_type=
77  to_struct_type(tmp_type);
78 
79  // enter struct scope
80  cpp_save_scopet save_scope(cpp_scopes);
81  cpp_scopes.set_scope(struct_type.get(ID_name));
82 
83  // find name of destructor
84  const struct_typet::componentst &components=
85  struct_type.components();
86 
87  irep_idt dtor_name;
88 
89  for(const auto &c : components)
90  {
91  const typet &type = c.type();
92 
93  if(
94  !c.get_bool(ID_from_base) && type.id() == ID_code &&
95  to_code_type(type).return_type().id() == ID_destructor)
96  {
97  dtor_name = c.get_base_name();
98  break;
99  }
100  }
101 
102  // there is always a destructor for non-PODs
103  assert(dtor_name!="");
104 
105  cpp_namet cpp_name(dtor_name, source_location);
106 
107  exprt member(ID_member);
108  member.add(ID_component_cpp_name) = cpp_name;
109  member.copy_to_operands(object);
110 
111  side_effect_expr_function_callt function_call;
112  function_call.add_source_location()=source_location;
113  function_call.function().swap(member);
114 
116  already_typechecked(function_call);
117 
118  new_code = code_expressiont(function_call);
119  new_code.add_source_location() = source_location;
120  }
121 
122  return new_code;
123 }
The type of an expression, extends irept.
Definition: type.h:27
BigInt mp_integer
Definition: mp_arith.h:22
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt&#39;s operands.
Definition: expr.h:123
std::vector< componentt > componentst
Definition: std_types.h:203
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt&#39;s operands.
Definition: expr.cpp:29
void already_typechecked(irept &irep)
Definition: cpp_util.h:18
const componentst & components() const
Definition: std_types.h:205
typet & type()
Return the type of the expression.
Definition: expr.h:68
Structure type, corresponds to C style structs.
Definition: std_types.h:276
codet representation of an expression statement.
Definition: std_code.h:1504
const irep_idt & id() const
Definition: irep.h:259
void elaborate_class_template(const typet &type)
elaborate class template instances
optionalt< codet > cpp_destructor(const source_locationt &source_location, const exprt &object)
source_locationt source_location
Definition: message.h:236
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
nonstd::optional< T > optionalt
Definition: optional.h:35
bool is_reference(const typet &type)
Returns true if the type is a reference.
Definition: std_types.cpp:132
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
mstreamt & error() const
Definition: message.h:386
const exprt & size() const
Definition: std_types.h:1010
C++ Language Type Checking.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
bitvector_typet index_type()
Definition: c_types.cpp:16
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:88
A side_effect_exprt representation of a function call side effect.
Definition: std_code.h:1691
static eomt eom
Definition: message.h:284
void set_statement(const irep_idt &statement)
Definition: std_code.h:51
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
virtual void make_constant_index(exprt &expr)
irept & add(const irep_namet &name)
Definition: irep.cpp:305
void swap(irept &irep)
Definition: irep.h:303
source_locationt & add_source_location()
Definition: expr.h:233
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void typecheck_side_effect_function_call(side_effect_expr_function_callt &) override
std::string to_string(const typet &) override
const typet & return_type() const
Definition: std_types.h:883
Array index operator.
Definition: std_expr.h:1595
cpp_scopest cpp_scopes