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 typet &type,
22  const exprt &object)
23 {
24  codet new_code;
25  new_code.add_source_location()=source_location;
26 
27  elaborate_class_template(object.type());
28 
29  typet tmp_type(follow(object.type()));
30 
31  assert(!is_reference(tmp_type));
32 
33  // PODs don't need a destructor
34  if(cpp_is_pod(tmp_type))
35  {
36  new_code.make_nil();
37  return new_code;
38  }
39 
40  if(tmp_type.id()==ID_array)
41  {
42  const exprt &size_expr=
43  to_array_type(tmp_type).size();
44 
45  if(size_expr.id()=="infinity")
46  {
47  // don't initialize
48  new_code.make_nil();
49  return new_code;
50  }
51 
52  exprt tmp_size=size_expr;
53  make_constant_index(tmp_size);
54 
55  mp_integer s;
56  if(to_integer(tmp_size, s))
57  {
58  error().source_location=source_location;
59  error() << "array size `" << to_string(size_expr)
60  << "' is not a constant" << eom;
61  throw 0;
62  }
63 
64  new_code.type().id(ID_code);
65  new_code.add_source_location()=source_location;
66  new_code.set_statement(ID_block);
67 
68  // for each element of the array, call the destructor
69  for(mp_integer i=0; i < s; ++i)
70  {
71  exprt constant=from_integer(i, index_type());
72  constant.add_source_location()=source_location;
73 
74  index_exprt index(object, constant);
75  index.add_source_location()=source_location;
76 
77  exprt i_code =
78  cpp_destructor(source_location, tmp_type.subtype(), index);
79 
80  new_code.move_to_operands(i_code);
81  }
82  }
83  else
84  {
85  const struct_typet &struct_type=
86  to_struct_type(tmp_type);
87 
88  // enter struct scope
89  cpp_save_scopet save_scope(cpp_scopes);
90  cpp_scopes.set_scope(struct_type.get(ID_name));
91 
92  // find name of destructor
93  const struct_typet::componentst &components=
94  struct_type.components();
95 
96  irep_idt dtor_name;
97 
98  for(struct_typet::componentst::const_iterator
99  it=components.begin();
100  it!=components.end();
101  it++)
102  {
103  const typet &type=it->type();
104 
105  if(!it->get_bool(ID_from_base) &&
106  type.id()==ID_code &&
107  type.find(ID_return_type).id()==ID_destructor)
108  {
109  dtor_name=it->get(ID_base_name);
110  break;
111  }
112  }
113 
114  // there is always a destructor for non-PODs
115  assert(dtor_name!="");
116 
117  irept cpp_name(ID_cpp_name);
118  cpp_name.get_sub().push_back(irept(ID_name));
119  cpp_name.get_sub().back().set(ID_identifier, dtor_name);
120  cpp_name.get_sub().back().set(ID_C_source_location, source_location);
121 
122  side_effect_expr_function_callt function_call;
123  function_call.add_source_location()=source_location;
124  function_call.function().swap(static_cast<exprt&>(cpp_name));
125 
127  assert(function_call.get(ID_statement)==ID_temporary_object);
128 
129  exprt &initializer =
130  static_cast<exprt &>(function_call.add(ID_initializer));
131 
132  assert(initializer.id()==ID_code
133  && initializer.get(ID_statement)==ID_expression);
134 
136  to_side_effect_expr_function_call(initializer.op0());
137 
138  exprt &tmp_this=func_ini.arguments().front();
139  assert(tmp_this.id()==ID_address_of
140  && tmp_this.op0().id()=="new_object");
141 
142  tmp_this=address_of_exprt(object, pointer_type(object.type()));
143 
144  new_code.swap(initializer);
145  }
146 
147  return new_code;
148 }
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
Definition: std_code.h:1392
The type of an expression.
Definition: type.h:22
void typecheck_side_effect_function_call(side_effect_expr_function_callt &expr)
BigInt mp_integer
Definition: mp_arith.h:22
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
std::vector< componentt > componentst
Definition: std_types.h:243
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Structure type.
Definition: std_types.h:297
subt & get_sub()
Definition: irep.h:245
const irep_idt & id() const
Definition: irep.h:189
void elaborate_class_template(const typet &type)
elaborate class template instances
source_locationt source_location
Definition: message.h:214
bool cpp_is_pod(const typet &type) const
Definition: cpp_is_pod.cpp:14
bool is_reference(const typet &type)
TO_BE_DOCUMENTED.
Definition: std_types.cpp:105
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
codet cpp_destructor(const source_locationt &source_location, const typet &type, const exprt &object)
mstreamt & error() const
Definition: message.h:302
const exprt & size() const
Definition: std_types.h:1014
Base class for tree-like data structures with sharing.
Definition: irep.h:86
C++ Language Type Checking.
const typet & follow(const typet &) const
Definition: namespace.cpp:55
bitvector_typet index_type()
Definition: c_types.cpp:16
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
Operator to return the address of an object.
Definition: std_expr.h:3170
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:88
A function call side effect.
Definition: std_code.h:1352
void set_statement(const irep_idt &statement)
Definition: std_code.h:34
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
Base class for all expressions.
Definition: expr.h:42
virtual void make_constant_index(exprt &expr)
irept & add(const irep_namet &name)
Definition: irep.cpp:306
virtual std::string to_string(const typet &type)
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
source_locationt & add_source_location()
Definition: expr.h:130
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
A statement in a programming language.
Definition: std_code.h:21
const typet & subtype() const
Definition: type.h:33
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
array index operator
Definition: std_expr.h:1462
cpp_scopest cpp_scopes