|
23 | 23 |
|
24 | 24 | #include "symex_dereference_state.h"
|
25 | 25 |
|
26 |
| -void goto_symext::dereference_rec_address_of( |
27 |
| - exprt &expr, |
28 |
| - statet &state, |
29 |
| - guardt &guard) |
30 |
| -{ |
31 |
| - // Could be member, could be if, could be index. |
32 |
| - |
33 |
| - if(expr.id()==ID_member) |
34 |
| - dereference_rec_address_of( |
35 |
| - to_member_expr(expr).struct_op(), state, guard); |
36 |
| - else if(expr.id()==ID_if) |
37 |
| - { |
38 |
| - // the condition is not an address |
39 |
| - dereference_rec( |
40 |
| - to_if_expr(expr).cond(), state, guard, false); |
41 |
| - |
42 |
| - // add to guard? |
43 |
| - dereference_rec_address_of( |
44 |
| - to_if_expr(expr).true_case(), state, guard); |
45 |
| - dereference_rec_address_of( |
46 |
| - to_if_expr(expr).false_case(), state, guard); |
47 |
| - } |
48 |
| - else if(expr.id()==ID_index) |
49 |
| - { |
50 |
| - // the index is not an address |
51 |
| - dereference_rec( |
52 |
| - to_index_expr(expr).index(), state, guard, false); |
53 |
| - |
54 |
| - // the array _is_ an address |
55 |
| - dereference_rec_address_of( |
56 |
| - to_index_expr(expr).array(), state, guard); |
57 |
| - } |
58 |
| - else |
59 |
| - { |
60 |
| - // give up and dereference |
61 |
| - |
62 |
| - dereference_rec(expr, state, guard, false); |
63 |
| - } |
64 |
| -} |
65 |
| - |
66 |
| -bool goto_symext::is_index_member_symbol_if(const exprt &expr) |
67 |
| -{ |
68 |
| - // Could be member, could be if, could be index. |
69 |
| - |
70 |
| - if(expr.id()==ID_member) |
71 |
| - { |
72 |
| - return is_index_member_symbol_if( |
73 |
| - to_member_expr(expr).struct_op()); |
74 |
| - } |
75 |
| - else if(expr.id()==ID_if) |
76 |
| - { |
77 |
| - return |
78 |
| - is_index_member_symbol_if(to_if_expr(expr).true_case()) && |
79 |
| - is_index_member_symbol_if(to_if_expr(expr).false_case()); |
80 |
| - } |
81 |
| - else if(expr.id()==ID_index) |
82 |
| - { |
83 |
| - return is_index_member_symbol_if(to_index_expr(expr).array()); |
84 |
| - } |
85 |
| - else if(expr.id()==ID_symbol) |
86 |
| - return true; |
87 |
| - else |
88 |
| - return false; |
89 |
| -} |
90 |
| - |
91 | 26 | /// Evaluate an ID_address_of expression
|
92 | 27 | exprt goto_symext::address_arithmetic(
|
93 | 28 | const exprt &expr,
|
|
0 commit comments