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