cprover
Loading...
Searching...
No Matches
destructor.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Destructor Calls
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "destructor.h"
14
15#include <util/namespace.h>
16#include <util/pointer_expr.h>
17
19 const namespacet &ns,
20 const typet &type)
21{
22 if(type.id() == ID_struct_tag)
23 {
24 return get_destructor(ns, ns.follow_tag(to_struct_tag_type(type)));
25 }
26 else if(type.id()==ID_struct)
27 {
28 const exprt &methods=static_cast<const exprt&>(type.find(ID_methods));
29
30 for(const auto &op : methods.operands())
31 {
32 if(op.type().id() == ID_code)
33 {
34 const code_typet &code_type = to_code_type(op.type());
35
36 if(code_type.return_type().id()==ID_destructor &&
37 code_type.parameters().size()==1)
38 {
39 const typet &arg_type=code_type.parameters().front().type();
40
41 if(
42 arg_type.id() == ID_pointer &&
43 ns.follow(to_pointer_type(arg_type).base_type()) == type)
44 {
45 const symbol_exprt symbol_expr(op.get(ID_name), op.type());
46 return code_function_callt(symbol_expr);
47 }
48 }
49 }
50 }
51 }
52
53 return static_cast<const code_function_callt &>(get_nil_irep());
54}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
goto_instruction_codet representation of a function call statement.
Base type of functions.
Definition std_types.h:539
Base class for all expressions.
Definition expr.h:56
operandst & operands()
Definition expr.h:94
const irept & find(const irep_idt &name) const
Definition irep.cpp:101
const irep_idt & id() const
Definition irep.h:396
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Expression to hold a symbol (variable)
Definition std_expr.h:113
The type of an expression, extends irept.
Definition type.h:29
code_function_callt get_destructor(const namespacet &ns, const typet &type)
Destructor Calls.
const irept & get_nil_irep()
Definition irep.cpp:19
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition std_types.h:474