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  {
35  new_code.make_nil();
36  return new_code;
37  }
38 
39  if(tmp_type.id()==ID_array)
40  {
41  const exprt &size_expr=
42  to_array_type(tmp_type).size();
43 
44  if(size_expr.id()=="infinity")
45  {
46  // don't initialize
47  new_code.make_nil();
48  return new_code;
49  }
50 
51  exprt tmp_size=size_expr;
52  make_constant_index(tmp_size);
53 
54  mp_integer s;
55  if(to_integer(tmp_size, s))
56  {
57  error().source_location=source_location;
58  error() << "array size `" << to_string(size_expr)
59  << "' is not a constant" << eom;
60  throw 0;
61  }
62 
63  new_code.type().id(ID_code);
64  new_code.add_source_location()=source_location;
65  new_code.set_statement(ID_block);
66 
67  // for each element of the array, call the destructor
68  for(mp_integer i=0; i < s; ++i)
69  {
70  exprt constant=from_integer(i, index_type());
71  constant.add_source_location()=source_location;
72 
73  index_exprt index(object, constant);
74  index.add_source_location()=source_location;
75 
76  exprt i_code = cpp_destructor(source_location, index);
77 
78  new_code.move_to_operands(i_code);
79  }
80  }
81  else
82  {
83  const struct_typet &struct_type=
84  to_struct_type(tmp_type);
85 
86  // enter struct scope
87  cpp_save_scopet save_scope(cpp_scopes);
88  cpp_scopes.set_scope(struct_type.get(ID_name));
89 
90  // find name of destructor
91  const struct_typet::componentst &components=
92  struct_type.components();
93 
94  irep_idt dtor_name;
95 
96  for(struct_typet::componentst::const_iterator
97  it=components.begin();
98  it!=components.end();
99  it++)
100  {
101  const typet &type=it->type();
102 
103  if(!it->get_bool(ID_from_base) &&
104  type.id()==ID_code &&
105  type.find(ID_return_type).id()==ID_destructor)
106  {
107  dtor_name=it->get(ID_base_name);
108  break;
109  }
110  }
111 
112  // there is always a destructor for non-PODs
113  assert(dtor_name!="");
114 
115  irept cpp_name(ID_cpp_name);
116  cpp_name.get_sub().push_back(irept(ID_name));
117  cpp_name.get_sub().back().set(ID_identifier, dtor_name);
118  cpp_name.get_sub().back().set(ID_C_source_location, source_location);
119 
120  exprt member(ID_member);
121  member.add(ID_component_cpp_name) = cpp_name;
122  member.copy_to_operands(object);
123 
124  side_effect_expr_function_callt function_call;
125  function_call.add_source_location()=source_location;
126  function_call.function().swap(member);
127 
129  already_typechecked(function_call);
130 
131  new_code = code_expressiont(function_call);
132  new_code.add_source_location() = source_location;
133  }
134 
135  return new_code;
136 }
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
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
std::vector< componentt > componentst
Definition: std_types.h:243
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
void already_typechecked(irept &irep)
Definition: cpp_util.h:18
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
An expression statement.
Definition: std_code.h:1220
codet cpp_destructor(const source_locationt &source_location, const exprt &object)
subt & get_sub()
Definition: irep.h:317
const irep_idt & id() const
Definition: irep.h:259
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
mstreamt & error() const
Definition: message.h:302
const exprt & size() const
Definition: std_types.h:1023
Base class for tree-like data structures with sharing.
Definition: irep.h:156
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
cpp_scopet & set_scope(const irep_idt &identifier)
Definition: cpp_scopes.h:88
A function call side effect.
Definition: std_code.h:1395
void set_statement(const irep_idt &statement)
Definition: std_code.h:35
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
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:315
void swap(irept &irep)
Definition: irep.h:303
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
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