28 std::vector<codet> statements;
29 for(
auto sub_expression_it = function_value.
depth_begin();
30 sub_expression_it != function_value.
depth_end();
33 if(sub_expression_it->id() == ID_code)
35 statements.push_back(
to_code(*sub_expression_it));
44 const std::vector<codet>
49 const symbolt *entry_point_function =
51 REQUIRE(entry_point_function !=
nullptr);
69 const std::vector<codet> &statements,
77 for(
const auto &assignment : statements)
79 if(assignment.get_statement() == ID_assign)
83 if(code_assign.
lhs().
id() == ID_member)
87 if(superclass_name.has_value())
101 const irep_idt supercomponent_name =
102 "@" +
id2string(superclass_name.value());
106 ode.
build(superclass_expr, ns);
116 locations.null_assignment = code_assign;
120 locations.non_null_assignments.push_back(code_assign);
134 ode.
build(member_expr, ns);
144 locations.null_assignment = code_assign;
148 locations.non_null_assignments.push_back(code_assign);
166 const std::vector<codet> &statements,
171 for(
const auto &assignment : statements)
173 if(assignment.get_statement() == ID_assign)
177 if(code_assign.
lhs().
id() == ID_member)
182 member_expr.
op().
id() == ID_dereference)
186 pointer.id() == ID_symbol &&
218 const std::vector<codet> &instructions)
220 INFO(
"Looking for symbol: " << pointer_name);
221 std::regex special_chars{R
"([-[\]{}()*+?.,\^$|#\s])"};
222 std::string sanitized =
223 std::regex_replace(id2string(pointer_name), special_chars, R"(\$&)");
225 std::regex(
"^" + sanitized +
"$"), instructions);
230 const std::regex &pointer_name_match,
231 const std::vector<codet> &instructions)
234 bool found_assignment =
false;
235 std::vector<irep_idt> all_symbols;
236 for(
const codet &statement : instructions)
238 if(statement.get_statement() == ID_assign)
241 if(code_assign.
lhs().
id() == ID_symbol)
259 found_assignment =
true;
265 std::ostringstream found_symbols;
266 for(
const auto entry : all_symbols)
268 found_symbols << entry << std::endl;
270 INFO(
"Symbols: " << found_symbols.str());
271 REQUIRE(found_assignment);
284 const std::vector<codet> &entry_point_instructions)
286 for(
const auto &statement : entry_point_instructions)
288 if(statement.get_statement() == ID_decl)
292 if(decl_statement.get_identifier() == variable_name)
294 return decl_statement;
307 const std::vector<codet> &entry_point_instructions,
311 symbol_identifier, entry_point_instructions)
313 REQUIRE(assignments.size() == 1);
314 return assignments[0].rhs();
326 const std::vector<codet> &entry_point_instructions,
330 entry_point_instructions, symbol_identifier);
332 return expr_try_dynamic_cast<symbol_exprt>(
skip_typecast(expr));
351 const std::vector<codet> &entry_point_instructions,
352 const irep_idt &input_symbol_identifier)
356 entry_point_instructions, input_symbol_identifier);
358 if(symbol_assigned_to_input_symbol)
361 entry_point_instructions,
365 return input_symbol_identifier;
385 const irep_idt &component_type_name,
387 const std::vector<codet> &entry_point_instructions,
394 const auto &component_assignments =
396 entry_point_instructions,
402 "looking for component assignment " << component_name <<
" in "
404 REQUIRE(component_assignments.non_null_assignments.size() == 1);
409 const symbol_exprt *rhs_symbol_expr = expr_try_dynamic_cast<symbol_exprt>(
410 skip_typecast(component_assignments.non_null_assignments[0].rhs()));
411 REQUIRE(rhs_symbol_expr);
420 const auto &component_declaration =
422 symbol_identifier, entry_point_instructions);
423 const typet &component_type =
425 REQUIRE(component_type.
id() == ID_struct_tag);
426 const auto &component_struct =
428 REQUIRE(component_struct.get(ID_name) == component_type_name);
430 return symbol_identifier;
446 const irep_idt &array_component_name,
448 const std::vector<codet> &entry_point_instructions,
453 const auto &component_assignments =
455 entry_point_instructions,
458 array_component_name,
460 REQUIRE(component_assignments.non_null_assignments.size() == 1);
465 const exprt &component_assignment_rhs_expr =
466 component_assignments.non_null_assignments[0].rhs();
471 const auto &component_assignment_rhs =
473 const auto &component_reference_tmp_name =
477 REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
481 .
get(ID_identifier) == array_type_name);
485 const auto &component_reference_assignments =
487 component_reference_tmp_name, entry_point_instructions);
488 REQUIRE(component_reference_assignments.non_null_assignments.size() == 1);
489 const exprt &component_reference_assignment_rhs_expr =
490 component_reference_assignments.non_null_assignments[0].rhs();
493 PRECONDITION(component_reference_assignment_rhs_expr.
id() == ID_side_effect);
494 const auto &array_component_reference_assignment_rhs =
499 array_component_reference_assignment_rhs.type().id() == ID_pointer);
503 REQUIRE(array.
get(ID_identifier) == array_type_name);
505 return component_reference_tmp_name;
516 const std::vector<codet> &entry_point_statements)
524 entry_point_statements);
533 const auto &argument_assignment =
547 const std::vector<codet> &statements,
548 const irep_idt &function_call_identifier)
550 std::vector<code_function_callt> function_calls;
551 for(
const codet &statement : statements)
553 if(statement.get_statement() == ID_function_call)
558 if(function_call.
function().
id() == ID_symbol)
562 function_call_identifier)
564 function_calls.push_back(function_call);
569 return function_calls;