cprover
object_id.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Object Identifiers
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "object_id.h"
13 
14 #include <util/pointer_expr.h>
15 #include <util/std_code.h>
16 
17 enum class get_modet { LHS_R, LHS_W, READ };
18 
20  get_modet mode,
21  const exprt &expr,
22  object_id_sett &dest,
23  const std::string &suffix)
24 {
25  if(expr.id()==ID_symbol)
26  {
27  if(mode==get_modet::LHS_W || mode==get_modet::READ)
28  dest.insert(object_idt(to_symbol_expr(expr)));
29  }
30  else if(expr.id()==ID_index)
31  {
32  const index_exprt &index_expr=to_index_expr(expr);
33 
34  if(mode==get_modet::LHS_R || mode==get_modet::READ)
35  get_objects_rec(get_modet::READ, index_expr.index(), dest, "");
36 
37  if(mode==get_modet::LHS_R)
38  get_objects_rec(get_modet::READ, index_expr.array(), dest, "[]"+suffix);
39  else
40  get_objects_rec(mode, index_expr.array(), dest, "[]"+suffix);
41  }
42  else if(expr.id()==ID_if)
43  {
44  const if_exprt &if_expr=to_if_expr(expr);
45 
46  if(mode==get_modet::LHS_R || mode==get_modet::READ)
47  get_objects_rec(get_modet::READ, if_expr.cond(), dest, "");
48 
49  get_objects_rec(mode, if_expr.true_case(), dest, suffix);
50  get_objects_rec(mode, if_expr.false_case(), dest, suffix);
51  }
52  else if(expr.id()==ID_member)
53  {
54  const member_exprt &member_expr=to_member_expr(expr);
55 
56  get_objects_rec(mode, member_expr.struct_op(), dest,
57  "."+id2string(member_expr.get_component_name())+suffix);
58  }
59  else if(expr.id()==ID_dereference)
60  {
61  const dereference_exprt &dereference_expr=
62  to_dereference_expr(expr);
63 
64  if(mode==get_modet::LHS_R || mode==get_modet::READ)
65  get_objects_rec(get_modet::READ, dereference_expr.pointer(), dest, "");
66  }
67  else
68  {
69  if(mode==get_modet::LHS_R || mode==get_modet::READ)
70  forall_operands(it, expr)
71  get_objects_rec(get_modet::READ, *it, dest, "");
72  }
73 }
74 
75 void get_objects(const exprt &expr, object_id_sett &dest)
76 {
77  get_objects_rec(get_modet::READ, expr, dest, "");
78 }
79 
80 void get_objects_r(const code_assignt &assign, object_id_sett &dest)
81 {
82  get_objects_rec(get_modet::LHS_R, assign.lhs(), dest, "");
83  get_objects_rec(get_modet::READ, assign.rhs(), dest, "");
84 }
85 
86 void get_objects_w(const code_assignt &assign, object_id_sett &dest)
87 {
88  get_objects_rec(get_modet::LHS_W, assign.lhs(), dest, "");
89 }
90 
91 void get_objects_w(const exprt &lhs, object_id_sett &dest)
92 {
93  get_objects_rec(get_modet::LHS_W, lhs, dest, "");
94 }
95 
96 void get_objects_r_lhs(const exprt &lhs, object_id_sett &dest)
97 {
98  get_objects_rec(get_modet::LHS_R, lhs, dest, "");
99 }
A codet representing an assignment in the program.
Definition: std_code.h:293
exprt & rhs()
Definition: std_code.h:315
exprt & lhs()
Definition: std_code.h:310
Operator to dereference a pointer.
Definition: pointer_expr.h:628
Base class for all expressions.
Definition: expr.h:54
The trinary if-then-else operator.
Definition: std_expr.h:2172
exprt & true_case()
Definition: std_expr.h:2199
exprt & false_case()
Definition: std_expr.h:2209
exprt & cond()
Definition: std_expr.h:2189
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1344
exprt & index()
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:407
Extract member of struct or union.
Definition: std_expr.h:2613
const exprt & struct_op() const
Definition: std_expr.h:2643
irep_idt get_component_name() const
Definition: std_expr.h:2627
#define forall_operands(it, expr)
Definition: expr.h:18
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
get_modet
Definition: object_id.cpp:17
void get_objects_r_lhs(const exprt &lhs, object_id_sett &dest)
Definition: object_id.cpp:96
void get_objects(const exprt &expr, object_id_sett &dest)
Definition: object_id.cpp:75
void get_objects_r(const code_assignt &assign, object_id_sett &dest)
Definition: object_id.cpp:80
void get_objects_rec(get_modet mode, const exprt &expr, object_id_sett &dest, const std::string &suffix)
Definition: object_id.cpp:19
void get_objects_w(const code_assignt &assign, object_id_sett &dest)
Definition: object_id.cpp:86
Object Identifiers.
std::set< object_idt > object_id_sett
Definition: object_id.h:58
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:684
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382