cprover
destructor.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Destructor Calls
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "destructor.h"
13 
14 #include <util/std_types.h>
15 #include <util/std_code.h>
16 
18  const namespacet &ns,
19  const typet &type)
20 {
21  if(type.id()==ID_symbol)
22  {
23  return get_destructor(ns, ns.follow(type));
24  }
25  else if(type.id()==ID_struct)
26  {
27  const exprt &methods=static_cast<const exprt&>(type.find(ID_methods));
28 
29  forall_operands(it, methods)
30  {
31  if(it->type().id()==ID_code)
32  {
33  const code_typet &code_type=to_code_type(it->type());
34 
35  if(code_type.return_type().id()==ID_destructor &&
36  code_type.parameters().size()==1)
37  {
38  const typet &arg_type=code_type.parameters().front().type();
39 
40  if(arg_type.id()==ID_pointer &&
41  ns.follow(arg_type.subtype())==type)
42  {
43  exprt symbol_expr(ID_symbol, it->type());
44  symbol_expr.set(ID_identifier, it->get(ID_name));
45 
46  code_function_callt function_call;
47  function_call.function()=symbol_expr;
48 
49  return function_call;
50  }
51  }
52  }
53  }
54  }
55 
56  return static_cast<const code_function_callt &>(get_nil_irep());
57 }
const irept & get_nil_irep()
Definition: irep.cpp:56
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
Base type of functions.
Definition: std_types.h:734
Destructor Calls.
const irep_idt & id() const
Definition: irep.h:189
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A function call.
Definition: std_code.h:657
#define forall_operands(it, expr)
Definition: expr.h:17
API to type classes.
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
code_function_callt get_destructor(const namespacet &ns, const typet &type)
Definition: destructor.cpp:17
const typet & subtype() const
Definition: type.h:31
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const typet & return_type() const
Definition: std_types.h:831
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214