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;
The type of an expression, extends irept.
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 & 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, const symbol_tablet &symbol_table)
Checks that the component of the structure (possibly inherited from the superclass) is assigned an ob...
const irep_idt & get_identifier() const
Goto Programs with Functions.
const std::vector< codet > require_entry_point_statements(const symbol_tablet &symbol_table)
The null pointer constant.
exprt value
Initial value of symbol.
typet & type()
Return the type of the expression.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
depth_iteratort depth_begin()
Forward depth-first search iterators These iterators' copy operations are expensive,...
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)
const irep_idt & id() const
A codet representing the declaration of a local variable.
nonstd::optional< T > optionalt
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 std::vector< codet > &entry_point_instructions, const symbol_tablet &symbol_table)
Checks that the array component of the structure (possibly inherited from the superclass) is assigned...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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, const symbol_tablet &symbol_table)
Find assignment statements of the form:
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Split an expression into a base object and a (byte) offset.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
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
codet representation of a function call statement.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an 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 typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
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 an 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 typet to a pointer_typet.
Utilties for inspecting goto functions.
Data structure for representing an arbitrary statement in a program.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
optionalt< code_assignt > null_assignment
A codet representing an assignment in the program.
const code_function_callt & to_code_function_call(const codet &code)