11 #include <testing-utils/catch.hpp>
26 std::vector<codet> statements;
27 for(
auto sub_expression_it = function_value.
depth_begin();
28 sub_expression_it != function_value.
depth_end();
31 if(sub_expression_it->id() == ID_code)
33 statements.push_back(
to_code(*sub_expression_it));
42 const std::vector<codet>
47 const symbolt *entry_point_function =
49 REQUIRE(entry_point_function !=
nullptr);
67 const std::vector<codet> &statements,
75 for(
const auto &assignment : statements)
77 if(assignment.get_statement() == ID_assign)
81 if(code_assign.
lhs().
id() == ID_member)
85 if(superclass_name.has_value())
100 "@" +
id2string(superclass_name.value());
104 ode.build(superclass_expr, ns);
130 member_expr.
op().
id() == ID_symbol &&
160 const std::vector<codet> &statements,
165 for(
const auto &assignment : statements)
167 if(assignment.get_statement() == ID_assign)
171 if(code_assign.
lhs().
id() == ID_member)
176 member_expr.
op().
id() == ID_dereference &&
177 member_expr.
op().
op0().
id() == ID_symbol &&
208 const std::vector<codet> &instructions)
210 INFO(
"Looking for symbol: " << pointer_name);
211 std::regex special_chars{R
"([-[\]{}()*+?.,\^$|#\s])"};
212 std::string sanitized =
213 std::regex_replace(id2string(pointer_name), special_chars, R"(\$&)");
215 std::regex(
"^" + sanitized +
"$"), instructions);
220 const std::regex &pointer_name_match,
221 const std::vector<codet> &instructions)
224 bool found_assignment =
false;
225 std::vector<irep_idt> all_symbols;
226 for(
const codet &statement : instructions)
228 if(statement.get_statement() == ID_assign)
231 if(code_assign.
lhs().
id() == ID_symbol)
249 found_assignment =
true;
255 std::ostringstream found_symbols;
256 for(
const auto entry : all_symbols)
258 found_symbols << entry << std::endl;
260 INFO(
"Symbols: " << found_symbols.str());
261 REQUIRE(found_assignment);
274 const std::vector<codet> &entry_point_instructions)
276 for(
const auto &statement : entry_point_instructions)
278 if(statement.get_statement() == ID_decl)
282 if(decl_statement.get_identifier() == variable_name)
284 return decl_statement;
306 const irep_idt &component_type_name,
308 const std::vector<codet> &entry_point_instructions,
313 const auto &component_assignments =
315 entry_point_instructions,
320 REQUIRE(component_assignments.non_null_assignments.size() == 1);
328 exprt component_assignment_rhs_expr =
329 component_assignments.non_null_assignments[0].rhs();
333 if(component_assignment_rhs_expr.id() == ID_typecast)
335 const auto &component_assignment_rhs =
339 if(typecast_name.has_value())
341 REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
345 .get(ID_identifier) == typecast_name.value());
348 const auto &component_reference_tmp_name =
350 const auto &component_reference_assignments =
352 component_reference_tmp_name, entry_point_instructions)
354 REQUIRE(component_reference_assignments.size() == 1);
355 component_assignment_rhs_expr = component_reference_assignments[0].rhs();
359 const auto &component_reference_assignment_rhs =
361 const auto &component_tmp_name =
362 to_symbol_expr(component_reference_assignment_rhs.op()).get_identifier();
369 const auto &component_declaration =
371 component_tmp_name, entry_point_instructions);
372 REQUIRE(component_declaration.symbol().type().id() == ID_struct);
373 const auto &component_struct =
375 REQUIRE(component_struct.get(ID_name) == component_type_name);
377 return component_tmp_name;
393 const irep_idt &array_component_name,
395 const std::vector<codet> &entry_point_instructions,
400 const auto &component_assignments =
402 entry_point_instructions,
405 array_component_name,
407 REQUIRE(component_assignments.non_null_assignments.size() == 1);
412 const exprt &component_assignment_rhs_expr =
413 component_assignments.non_null_assignments[0].rhs();
417 PRECONDITION(component_assignment_rhs_expr.id() == ID_typecast);
418 const auto &component_assignment_rhs =
420 const auto &component_reference_tmp_name =
424 REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
428 .get(ID_identifier) == array_type_name);
432 const auto &component_reference_assignments =
434 component_reference_tmp_name, entry_point_instructions);
435 REQUIRE(component_reference_assignments.non_null_assignments.size() == 1);
436 const exprt &component_reference_assignment_rhs_expr =
437 component_reference_assignments.non_null_assignments[0].rhs();
440 PRECONDITION(component_reference_assignment_rhs_expr.id() == ID_side_effect);
441 const auto &array_component_reference_assignment_rhs =
446 array_component_reference_assignment_rhs.type().id() == ID_pointer);
448 to_pointer_type(array_component_reference_assignment_rhs.type()).subtype();
450 REQUIRE(array.get(ID_identifier) == array_type_name);
452 return component_reference_tmp_name;
463 const std::vector<codet> &entry_point_statements)
471 entry_point_statements);
480 const auto &argument_assignment =
482 const auto &argument_tmp_name =
485 return argument_tmp_name;
495 const std::vector<codet> &statements,
496 const irep_idt &function_call_identifier)
498 std::vector<code_function_callt> function_calls;
499 for(
const codet &statement : statements)
501 if(statement.get_statement() == ID_function_call)
506 if(function_call.
function().
id() == ID_symbol)
510 function_call_identifier)
512 function_calls.push_back(function_call);
517 return function_calls;