CBMC
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 
15 
16 #include <util/pointer_expr.h>
17 
18 enum class get_modet { LHS_R, LHS_W, READ };
19 
21  get_modet mode,
22  const exprt &expr,
23  object_id_sett &dest,
24  const std::string &suffix)
25 {
26  if(expr.id()==ID_symbol)
27  {
28  if(mode==get_modet::LHS_W || mode==get_modet::READ)
29  dest.insert(object_idt(to_symbol_expr(expr)));
30  }
31  else if(expr.id()==ID_index)
32  {
33  const index_exprt &index_expr=to_index_expr(expr);
34 
35  if(mode==get_modet::LHS_R || mode==get_modet::READ)
36  get_objects_rec(get_modet::READ, index_expr.index(), dest, "");
37 
38  if(mode==get_modet::LHS_R)
39  get_objects_rec(get_modet::READ, index_expr.array(), dest, "[]"+suffix);
40  else
41  get_objects_rec(mode, index_expr.array(), dest, "[]"+suffix);
42  }
43  else if(expr.id()==ID_if)
44  {
45  const if_exprt &if_expr=to_if_expr(expr);
46 
47  if(mode==get_modet::LHS_R || mode==get_modet::READ)
48  get_objects_rec(get_modet::READ, if_expr.cond(), dest, "");
49 
50  get_objects_rec(mode, if_expr.true_case(), dest, suffix);
51  get_objects_rec(mode, if_expr.false_case(), dest, suffix);
52  }
53  else if(expr.id()==ID_member)
54  {
55  const member_exprt &member_expr=to_member_expr(expr);
56 
57  get_objects_rec(mode, member_expr.struct_op(), dest,
58  "."+id2string(member_expr.get_component_name())+suffix);
59  }
60  else if(expr.id()==ID_dereference)
61  {
62  const dereference_exprt &dereference_expr=
63  to_dereference_expr(expr);
64 
65  if(mode==get_modet::LHS_R || mode==get_modet::READ)
66  get_objects_rec(get_modet::READ, dereference_expr.pointer(), dest, "");
67  }
68  else
69  {
70  if(mode==get_modet::LHS_R || mode==get_modet::READ)
71  {
72  for(const auto &op : expr.operands())
73  get_objects_rec(get_modet::READ, op, dest, "");
74  }
75  }
76 }
77 
78 void get_objects(const exprt &expr, object_id_sett &dest)
79 {
80  get_objects_rec(get_modet::READ, expr, dest, "");
81 }
82 
83 void get_objects_r(const code_assignt &assign, object_id_sett &dest)
84 {
85  get_objects_rec(get_modet::LHS_R, assign.lhs(), dest, "");
86  get_objects_rec(get_modet::READ, assign.rhs(), dest, "");
87 }
88 
89 void get_objects_w(const code_assignt &assign, object_id_sett &dest)
90 {
91  get_objects_rec(get_modet::LHS_W, assign.lhs(), dest, "");
92 }
93 
94 void get_objects_w(const exprt &lhs, object_id_sett &dest)
95 {
96  get_objects_rec(get_modet::LHS_W, lhs, dest, "");
97 }
98 
99 void get_objects_r_lhs(const exprt &lhs, object_id_sett &dest)
100 {
101  get_objects_rec(get_modet::LHS_R, lhs, dest, "");
102 }
A goto_instruction_codet representing an assignment in the program.
Operator to dereference a pointer.
Definition: pointer_expr.h:834
Base class for all expressions.
Definition: expr.h:56
operandst & operands()
Definition: expr.h:94
The trinary if-then-else operator.
Definition: std_expr.h:2370
exprt & true_case()
Definition: std_expr.h:2397
exprt & false_case()
Definition: std_expr.h:2407
exprt & cond()
Definition: std_expr.h:2387
Array index operator.
Definition: std_expr.h:1465
exprt & array()
Definition: std_expr.h:1495
exprt & index()
Definition: std_expr.h:1505
const irep_idt & id() const
Definition: irep.h:388
Extract member of struct or union.
Definition: std_expr.h:2844
const exprt & struct_op() const
Definition: std_expr.h:2882
irep_idt get_component_name() const
Definition: std_expr.h:2866
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
get_modet
Definition: object_id.cpp:18
void get_objects_r_lhs(const exprt &lhs, object_id_sett &dest)
Definition: object_id.cpp:99
void get_objects(const exprt &expr, object_id_sett &dest)
Definition: object_id.cpp:78
void get_objects_r(const code_assignt &assign, object_id_sett &dest)
Definition: object_id.cpp:83
void get_objects_rec(get_modet mode, const exprt &expr, object_id_sett &dest, const std::string &suffix)
Definition: object_id.cpp:20
void get_objects_w(const code_assignt &assign, object_id_sett &dest)
Definition: object_id.cpp:89
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:890
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2450
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2936
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533