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 enum class get_modet { LHS_R, LHS_W, READ };
15 
17  get_modet mode,
18  const exprt &expr,
19  object_id_sett &dest,
20  const std::string &suffix)
21 {
22  if(expr.id()==ID_symbol)
23  {
24  if(mode==get_modet::LHS_W || mode==get_modet::READ)
25  dest.insert(object_idt(to_symbol_expr(expr)));
26  }
27  else if(expr.id()==ID_index)
28  {
29  const index_exprt &index_expr=to_index_expr(expr);
30 
31  if(mode==get_modet::LHS_R || mode==get_modet::READ)
32  get_objects_rec(get_modet::READ, index_expr.index(), dest, "");
33 
34  if(mode==get_modet::LHS_R)
35  get_objects_rec(get_modet::READ, index_expr.array(), dest, "[]"+suffix);
36  else
37  get_objects_rec(mode, index_expr.array(), dest, "[]"+suffix);
38  }
39  else if(expr.id()==ID_if)
40  {
41  const if_exprt &if_expr=to_if_expr(expr);
42 
43  if(mode==get_modet::LHS_R || mode==get_modet::READ)
44  get_objects_rec(get_modet::READ, if_expr.cond(), dest, "");
45 
46  get_objects_rec(mode, if_expr.true_case(), dest, suffix);
47  get_objects_rec(mode, if_expr.false_case(), dest, suffix);
48  }
49  else if(expr.id()==ID_member)
50  {
51  const member_exprt &member_expr=to_member_expr(expr);
52 
53  get_objects_rec(mode, member_expr.struct_op(), dest,
54  "."+id2string(member_expr.get_component_name())+suffix);
55  }
56  else if(expr.id()==ID_dereference)
57  {
58  const dereference_exprt &dereference_expr=
59  to_dereference_expr(expr);
60 
61  if(mode==get_modet::LHS_R || mode==get_modet::READ)
62  get_objects_rec(get_modet::READ, dereference_expr.pointer(), dest, "");
63  }
64  else
65  {
66  if(mode==get_modet::LHS_R || mode==get_modet::READ)
67  forall_operands(it, expr)
68  get_objects_rec(get_modet::READ, *it, dest, "");
69  }
70 }
71 
72 void get_objects(const exprt &expr, object_id_sett &dest)
73 {
74  get_objects_rec(get_modet::READ, expr, dest, "");
75 }
76 
77 void get_objects_r(const code_assignt &assign, object_id_sett &dest)
78 {
79  get_objects_rec(get_modet::LHS_R, assign.lhs(), dest, "");
80  get_objects_rec(get_modet::READ, assign.rhs(), dest, "");
81 }
82 
83 void get_objects_w(const code_assignt &assign, object_id_sett &dest)
84 {
85  get_objects_rec(get_modet::LHS_W, assign.lhs(), dest, "");
86 }
87 
88 void get_objects_w(const exprt &lhs, object_id_sett &dest)
89 {
90  get_objects_rec(get_modet::LHS_W, lhs, dest, "");
91 }
92 
93 void get_objects_r_lhs(const exprt &lhs, object_id_sett &dest)
94 {
95  get_objects_rec(get_modet::LHS_R, lhs, dest, "");
96 }
get_modet
get_modet
Definition: object_id.cpp:14
get_modet::READ
@ READ
get_objects_w
void get_objects_w(const code_assignt &assign, object_id_sett &dest)
Definition: object_id.cpp:83
get_objects
void get_objects(const exprt &expr, object_id_sett &dest)
Definition: object_id.cpp:72
get_objects_rec
void get_objects_rec(get_modet mode, const exprt &expr, object_id_sett &dest, const std::string &suffix)
Definition: object_id.cpp:16
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3029
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
get_modet::LHS_W
@ LHS_W
get_modet::LHS_R
@ LHS_R
exprt
Base class for all expressions.
Definition: expr.h:53
object_idt
Definition: object_id.h:22
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
object_id.h
Object Identifiers.
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
member_exprt::struct_op
const exprt & struct_op() const
Definition: std_expr.h:3435
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:2901
get_objects_r
void get_objects_r(const code_assignt &assign, object_id_sett &dest)
Definition: object_id.cpp:77
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
get_objects_r_lhs
void get_objects_r_lhs(const exprt &lhs, object_id_sett &dest)
Definition: object_id.cpp:93
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
object_id_sett
std::set< object_idt > object_id_sett
Definition: object_id.h:57
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
member_exprt::get_component_name
irep_idt get_component_name() const
Definition: std_expr.h:3419
index_exprt
Array index operator.
Definition: std_expr.h:1293
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295