|
13 | 13 | #include <util/expr_iterator.h>
|
14 | 14 | #include <goto-programs/goto_functions.h>
|
15 | 15 | #include <java_bytecode/java_types.h>
|
| 16 | +#include <util/suffix.h> |
16 | 17 |
|
17 | 18 | /// Expand value of a function to include all child codets
|
18 | 19 | /// \param function_value: The value of the function (e.g. got by looking up
|
@@ -141,6 +142,53 @@ require_goto_statements::find_struct_component_assignments(
|
141 | 142 | return locations;
|
142 | 143 | }
|
143 | 144 |
|
| 145 | +/// Find assignment statements that set this->{component_name} |
| 146 | +/// \param statements The statements to look through |
| 147 | +/// \param component_name The name of the component whose assignments we are |
| 148 | +/// looking for. |
| 149 | +/// \return A collection of all non-null assignments to this component |
| 150 | +/// and, if present, a null assignment. |
| 151 | +require_goto_statements::pointer_assignment_locationt |
| 152 | +require_goto_statements::find_this_component_assignment( |
| 153 | + const std::vector<codet> &statements, |
| 154 | + const irep_idt &component_name) |
| 155 | +{ |
| 156 | + pointer_assignment_locationt locations; |
| 157 | + |
| 158 | + for(const auto &assignment : statements) |
| 159 | + { |
| 160 | + if(assignment.get_statement() == ID_assign) |
| 161 | + { |
| 162 | + const code_assignt &code_assign = to_code_assign(assignment); |
| 163 | + |
| 164 | + if(code_assign.lhs().id() == ID_member) |
| 165 | + { |
| 166 | + const member_exprt &member_expr = to_member_expr(code_assign.lhs()); |
| 167 | + if( |
| 168 | + member_expr.get_component_name() == component_name && |
| 169 | + member_expr.op().id() == ID_dereference && |
| 170 | + member_expr.op().op0().id() == ID_symbol && |
| 171 | + has_suffix( |
| 172 | + id2string(to_symbol_expr(member_expr.op().op0()).get_identifier()), |
| 173 | + "this")) |
| 174 | + { |
| 175 | + if( |
| 176 | + code_assign.rhs() == |
| 177 | + null_pointer_exprt(to_pointer_type(code_assign.lhs().type()))) |
| 178 | + { |
| 179 | + locations.null_assignment = code_assign; |
| 180 | + } |
| 181 | + else |
| 182 | + { |
| 183 | + locations.non_null_assignments.push_back(code_assign); |
| 184 | + } |
| 185 | + } |
| 186 | + } |
| 187 | + } |
| 188 | + } |
| 189 | + return locations; |
| 190 | +} |
| 191 | + |
144 | 192 | /// For a given variable name, gets the assignments to it in the provided
|
145 | 193 | /// instructions.
|
146 | 194 | /// \param pointer_name: The name of the variable
|
|
0 commit comments