cprover
Loading...
Searching...
No Matches
object_id.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Object Identifiers
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "object_id.h"
13
15
16#include <util/pointer_expr.h>
17
18enum 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=
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 forall_operands(it, expr)
72 get_objects_rec(get_modet::READ, *it, dest, "");
73 }
74}
75
76void get_objects(const exprt &expr, object_id_sett &dest)
77{
78 get_objects_rec(get_modet::READ, expr, dest, "");
79}
80
81void get_objects_r(const code_assignt &assign, object_id_sett &dest)
82{
83 get_objects_rec(get_modet::LHS_R, assign.lhs(), dest, "");
84 get_objects_rec(get_modet::READ, assign.rhs(), dest, "");
85}
86
87void get_objects_w(const code_assignt &assign, object_id_sett &dest)
88{
89 get_objects_rec(get_modet::LHS_W, assign.lhs(), dest, "");
90}
91
92void get_objects_w(const exprt &lhs, object_id_sett &dest)
93{
94 get_objects_rec(get_modet::LHS_W, lhs, dest, "");
95}
96
97void get_objects_r_lhs(const exprt &lhs, object_id_sett &dest)
98{
99 get_objects_rec(get_modet::LHS_R, lhs, dest, "");
100}
A codet representing an assignment in the program.
Operator to dereference a pointer.
Definition: pointer_expr.h:648
Base class for all expressions.
Definition: expr.h:54
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & cond()
Definition: std_expr.h:2243
exprt & false_case()
Definition: std_expr.h:2263
exprt & true_case()
Definition: std_expr.h:2253
Array index operator.
Definition: std_expr.h:1328
exprt & index()
Definition: std_expr.h:1363
exprt & array()
Definition: std_expr.h:1353
const irep_idt & id() const
Definition: irep.h:396
Extract member of struct or union.
Definition: std_expr.h:2667
const exprt & struct_op() const
Definition: std_expr.h:2697
irep_idt get_component_name() const
Definition: std_expr.h:2681
#define forall_operands(it, expr)
Definition: expr.h:18
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
get_modet
Definition: object_id.cpp:18
void get_objects_r_lhs(const exprt &lhs, object_id_sett &dest)
Definition: object_id.cpp:97
void get_objects(const exprt &expr, object_id_sett &dest)
Definition: object_id.cpp:76
void get_objects_r(const code_assignt &assign, object_id_sett &dest)
Definition: object_id.cpp:81
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:87
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:704
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2751
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189