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);
66 const std::vector<codet> &statements,
73 for(
const auto &assignment : statements)
75 if(assignment.get_statement() == ID_assign)
79 if(code_assign.
lhs().
id() == ID_member)
83 if(superclass_name.has_value())
124 member_expr.
op().
id() == ID_symbol &&
154 const std::vector<codet> &statements,
159 for(
const auto &assignment : statements)
161 if(assignment.get_statement() == ID_assign)
165 if(code_assign.
lhs().
id() == ID_member)
170 member_expr.
op().
id() == ID_dereference &&
171 member_expr.
op().
op0().
id() == ID_symbol &&
202 const std::vector<codet> &instructions)
204 INFO(
"Looking for symbol: " << pointer_name);
205 std::regex special_chars{R
"([-[\]{}()*+?.,\^$|#\s])"}; 206 std::string sanitized = 207 std::regex_replace(id2string(pointer_name), special_chars, R"(\$&)"); 209 std::regex(
"^" + sanitized +
"$"), instructions);
214 const std::regex &pointer_name_match,
215 const std::vector<codet> &instructions)
218 bool found_assignment =
false;
219 std::vector<irep_idt> all_symbols;
220 for(
const codet &statement : instructions)
222 if(statement.get_statement() == ID_assign)
225 if(code_assign.
lhs().
id() == ID_symbol)
243 found_assignment =
true;
249 std::ostringstream found_symbols;
250 for(
const auto entry : all_symbols)
252 found_symbols << entry << std::endl;
254 INFO(
"Symbols: " << found_symbols.str());
255 REQUIRE(found_assignment);
268 const std::vector<codet> &entry_point_instructions)
270 for(
const auto &statement : entry_point_instructions)
272 if(statement.get_statement() == ID_decl)
276 if(decl_statement.get_identifier() == variable_name)
278 return decl_statement;
299 const irep_idt &component_type_name,
301 const std::vector<codet> &entry_point_instructions)
305 const auto &component_assignments =
307 entry_point_instructions,
311 REQUIRE(component_assignments.non_null_assignments.size() == 1);
319 exprt component_assignment_rhs_expr =
320 component_assignments.non_null_assignments[0].rhs();
324 if(component_assignment_rhs_expr.id() == ID_typecast)
326 const auto &component_assignment_rhs =
330 if(typecast_name.has_value())
332 REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
336 .
get(ID_identifier) == typecast_name.value());
339 const auto &component_reference_tmp_name =
341 const auto &component_reference_assignments =
343 component_reference_tmp_name, entry_point_instructions)
345 REQUIRE(component_reference_assignments.size() == 1);
346 component_assignment_rhs_expr = component_reference_assignments[0].rhs();
350 const auto &component_reference_assignment_rhs =
352 const auto &component_tmp_name =
353 to_symbol_expr(component_reference_assignment_rhs.op()).get_identifier();
360 const auto &component_declaration =
362 component_tmp_name, entry_point_instructions);
363 REQUIRE(component_declaration.symbol().type().id() == ID_struct);
364 const auto &component_struct =
366 REQUIRE(component_struct.get(ID_name) == component_type_name);
368 return component_tmp_name;
384 const irep_idt &array_component_name,
386 const irep_idt &array_component_element_type_name,
387 const std::vector<codet> &entry_point_instructions)
391 const auto &component_assignments =
393 entry_point_instructions,
396 array_component_name);
397 REQUIRE(component_assignments.non_null_assignments.size() == 1);
402 const exprt &component_assignment_rhs_expr =
403 component_assignments.non_null_assignments[0].rhs();
407 PRECONDITION(component_assignment_rhs_expr.id() == ID_typecast);
408 const auto &component_assignment_rhs =
410 const auto &component_reference_tmp_name =
414 REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
417 .
get(ID_identifier) == array_type_name);
421 const auto &component_reference_assignments =
423 component_reference_tmp_name, entry_point_instructions);
424 REQUIRE(component_reference_assignments.non_null_assignments.size() == 1);
425 const exprt &component_reference_assignment_rhs_expr =
426 component_reference_assignments.non_null_assignments[0].rhs();
429 PRECONDITION(component_reference_assignment_rhs_expr.id() == ID_side_effect);
430 const auto &array_component_reference_assignment_rhs =
435 array_component_reference_assignment_rhs.type().id() == ID_pointer);
437 to_pointer_type(array_component_reference_assignment_rhs.type()).subtype();
439 REQUIRE(array.get(ID_identifier) == array_type_name);
441 return component_reference_tmp_name;
452 const std::vector<codet> &entry_point_statements)
460 entry_point_statements);
469 const auto &argument_assignment =
471 const auto &argument_tmp_name =
474 return argument_tmp_name;
484 const std::vector<codet> &statements,
485 const irep_idt &function_call_identifier)
487 std::vector<code_function_callt> function_calls;
488 for(
const codet &statement : statements)
490 if(statement.get_statement() == ID_function_call)
495 if(function_call.
function().
id() == ID_symbol)
499 function_call_identifier)
501 function_calls.push_back(function_call);
506 return function_calls;
The type of an expression.
const symbol_exprt & symbol() const
const code_declt & to_code_decl(const codet &code)
const std::string & id2string(const irep_idt &d)
std::vector< codet > get_all_statements(const exprt &function_value)
Expand value of a function to include all child codets.
const irep_idt & get_identifier() const
Goto Programs with Functions.
const std::vector< codet > require_entry_point_statements(const symbol_tablet &symbol_table)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
The null pointer constant.
exprt value
Initial value of symbol.
const irep_idt & require_struct_component_assignment(const irep_idt &structure_name, const optionalt< irep_idt > &superclass_name, const irep_idt &component_name, const irep_idt &component_type_name, const optionalt< irep_idt > &typecast_name, const std::vector< codet > &entry_point_instructions)
Checks that the component of the structure (possibly inherited from the superclass) is assigned an ob...
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
depth_iteratort depth_begin()
bool is_java_array_tag(const irep_idt &tag)
See above.
pointer_assignment_locationt find_this_component_assignment(const std::vector< codet > &statements, const irep_idt &component_name)
Find assignment statements that set this->{component_name}.
side_effect_exprt & to_side_effect_expr(exprt &expr)
Extract member of struct or union.
const exprt & compound() const
const code_assignt & to_code_assign(const codet &code)
pointer_assignment_locationt find_struct_component_assignments(const std::vector< codet > &statements, const irep_idt &structure_name, const optionalt< irep_idt > &superclass_name, const irep_idt &component_name)
Find assignment statements of the form:
const irep_idt & id() const
A declaration of a local variable.
nonstd::optional< T > optionalt
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const irep_idt & require_entry_point_argument_assignment(const irep_idt &argument_name, const std::vector< codet > &entry_point_statements)
Checks that the input argument (of method under test) with given name is assigned a single non-null o...
std::vector< code_assignt > non_null_assignments
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const code_declt & require_declaration_of_name(const irep_idt &variable_name, const std::vector< codet > &entry_point_instructions)
Find the declaration of the specific variable.
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
const irep_idt & require_struct_array_component_assignment(const irep_idt &structure_name, const optionalt< irep_idt > &superclass_name, const irep_idt &array_component_name, const irep_idt &array_type_name, const irep_idt &array_component_element_type_name, const std::vector< codet > &entry_point_instructions)
Checks that the array component of the structure (possibly inherited from the superclass) is assigned...
static irep_idt entry_point()
pointer_assignment_locationt find_pointer_assignments(const irep_idt &pointer_name, const std::vector< codet > &instructions)
For a given variable name, gets the assignments to it in the provided instructions.
std::vector< code_function_callt > find_function_calls(const std::vector< codet > &statements, const irep_idt &function_call_identifier)
Verify that a collection of statements contains a function call to a function whose symbol identifier...
Base class for all expressions.
irep_idt get_component_name() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const codet & to_code(const exprt &expr)
Expression to hold a symbol (variable)
depth_iteratort depth_end()
const char * c_str() const
bool has_suffix(const std::string &s, const std::string &suffix)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
Utilties for inspecting goto functions.
A statement in a programming language.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
optionalt< code_assignt > null_assignment
const code_function_callt & to_code_function_call(const codet &code)