30 std::vector<codet> statements;
31 for(
auto sub_expression_it = function_value.
depth_begin();
32 sub_expression_it != function_value.
depth_end();
35 if(sub_expression_it->id() == ID_code)
37 statements.push_back(
to_code(*sub_expression_it));
46 const std::vector<codet>
51 const symbolt *entry_point_function =
53 REQUIRE(entry_point_function !=
nullptr);
71 const std::vector<codet> &statements,
79 for(
const auto &assignment : statements)
81 if(assignment.get_statement() == ID_assign)
85 if(code_assign.
lhs().
id() == ID_member)
89 if(superclass_name.has_value())
103 const irep_idt supercomponent_name =
104 "@" +
id2string(superclass_name.value());
108 ode.
build(superclass_expr, ns);
118 locations.null_assignment = code_assign;
122 locations.non_null_assignments.push_back(code_assign);
136 ode.
build(member_expr, ns);
146 locations.null_assignment = code_assign;
150 locations.non_null_assignments.push_back(code_assign);
168 const std::vector<codet> &statements,
173 for(
const auto &assignment : statements)
175 if(assignment.get_statement() == ID_assign)
179 if(code_assign.
lhs().
id() == ID_member)
184 member_expr.
op().
id() == ID_dereference)
188 pointer.id() == ID_symbol &&
220 const std::vector<codet> &instructions)
222 INFO(
"Looking for symbol: " << pointer_name);
223 std::regex special_chars{R
"([-[\]{}()*+?.,\^$|#\s])"};
224 std::string sanitized =
225 std::regex_replace(id2string(pointer_name), special_chars, R"(\$&)");
227 std::regex(
"^" + sanitized +
"$"), instructions);
232 const std::regex &pointer_name_match,
233 const std::vector<codet> &instructions)
236 bool found_assignment =
false;
237 std::vector<irep_idt> all_symbols;
238 for(
const codet &statement : instructions)
240 if(statement.get_statement() == ID_assign)
243 if(code_assign.
lhs().
id() == ID_symbol)
261 found_assignment =
true;
267 std::ostringstream found_symbols;
268 for(
const auto &entry : all_symbols)
270 found_symbols << entry << std::endl;
272 INFO(
"Symbols: " << found_symbols.str());
273 REQUIRE(found_assignment);
286 const std::vector<codet> &entry_point_instructions)
288 for(
const auto &statement : entry_point_instructions)
290 if(statement.get_statement() == ID_decl)
294 if(decl_statement.get_identifier() == variable_name)
296 return decl_statement;
309 const std::vector<codet> &entry_point_instructions,
313 symbol_identifier, entry_point_instructions)
315 REQUIRE(assignments.size() == 1);
316 return assignments[0].rhs();
328 const std::vector<codet> &entry_point_instructions,
332 entry_point_instructions, symbol_identifier);
334 return expr_try_dynamic_cast<symbol_exprt>(
skip_typecast(expr));
353 const std::vector<codet> &entry_point_instructions,
354 const irep_idt &input_symbol_identifier)
358 entry_point_instructions, input_symbol_identifier);
360 if(symbol_assigned_to_input_symbol)
363 entry_point_instructions,
367 return input_symbol_identifier;
387 const irep_idt &component_type_name,
389 const std::vector<codet> &entry_point_instructions,
396 const auto &component_assignments =
398 entry_point_instructions,
404 "looking for component assignment " << component_name <<
" in "
406 REQUIRE(component_assignments.non_null_assignments.size() == 1);
411 const symbol_exprt *rhs_symbol_expr = expr_try_dynamic_cast<symbol_exprt>(
412 skip_typecast(component_assignments.non_null_assignments[0].rhs()));
413 REQUIRE(rhs_symbol_expr);
422 const auto &component_declaration =
424 symbol_identifier, entry_point_instructions);
425 const typet &component_type =
427 REQUIRE(component_type.
id() == ID_struct_tag);
428 const auto &component_struct =
430 REQUIRE(component_struct.get(ID_name) == component_type_name);
432 return symbol_identifier;
448 const irep_idt &array_component_name,
450 const std::vector<codet> &entry_point_instructions,
455 const auto &component_assignments =
457 entry_point_instructions,
460 array_component_name,
462 REQUIRE(component_assignments.non_null_assignments.size() == 1);
467 const exprt &component_assignment_rhs_expr =
468 component_assignments.non_null_assignments[0].rhs();
473 const auto &component_assignment_rhs =
475 const auto &component_reference_tmp_name =
479 REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
483 .
get(ID_identifier) == array_type_name);
487 const auto &component_reference_assignments =
489 component_reference_tmp_name, entry_point_instructions);
490 REQUIRE(component_reference_assignments.non_null_assignments.size() == 1);
491 const exprt &component_reference_assignment_rhs_expr =
492 component_reference_assignments.non_null_assignments[0].rhs();
495 PRECONDITION(component_reference_assignment_rhs_expr.
id() == ID_side_effect);
496 const auto &array_component_reference_assignment_rhs =
501 array_component_reference_assignment_rhs.type().id() == ID_pointer);
505 REQUIRE(array.
get(ID_identifier) == array_type_name);
507 return component_reference_tmp_name;
518 const std::vector<codet> &entry_point_statements)
526 entry_point_statements);
535 const auto &argument_assignment =
549 const std::vector<codet> &statements,
550 const irep_idt &function_call_identifier)
552 std::vector<code_function_callt> function_calls;
553 for(
const codet &statement : statements)
555 if(statement.get_statement() == ID_function_call)
560 if(function_call.
function().
id() == ID_symbol)
564 function_call_identifier)
566 function_calls.push_back(function_call);
571 return function_calls;
A codet representing an assignment in the program.
A codet representing the declaration of a local variable.
codet representation of a function call statement.
Data structure for representing an arbitrary statement in a program.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const char * c_str() const
Base class for all expressions.
depth_iteratort depth_end()
depth_iteratort depth_begin()
typet & type()
Return the type of the expression.
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) const
Extract member of struct or union.
const exprt & compound() const
irep_idt get_component_name() const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
Split an expression into a base object and a (byte) offset.
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
static const exprt & root_object(const exprt &expr)
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
exprt value
Initial value of symbol.
The type of an expression, extends irept.
const typet & subtype() const
Forward depth-first search iterators These iterators' copy operations are expensive,...
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Deprecated expression utility functions.
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
bool is_java_array_tag(const irep_idt &tag)
See above.
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...
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...
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 & 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...
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.
const std::vector< codet > require_entry_point_statements(const symbol_tablet &symbol_table)
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}.
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:
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.
nonstd::optional< T > optionalt
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const symbol_exprt * try_get_unique_symbol_assigned_to_symbol(const std::vector< codet > &entry_point_instructions, const irep_idt &symbol_identifier)
Get the unique symbol assigned to a symbol, if one exists.
static const irep_idt & get_ultimate_source_symbol(const std::vector< codet > &entry_point_instructions, const irep_idt &input_symbol_identifier)
Follow the chain of non-null assignments until we find a symbol that hasn't ever had another symbol a...
const exprt & get_unique_non_null_expression_assigned_to_symbol(const std::vector< codet > &entry_point_instructions, const irep_idt &symbol_identifier)
Get the unique non-null expression assigned to a symbol.
Utilties for inspecting goto functions.
#define PRECONDITION(CONDITION)
side_effect_exprt & to_side_effect_expr(exprt &expr)
const codet & to_code(const exprt &expr)
const code_declt & to_code_decl(const codet &code)
const code_function_callt & to_code_function_call(const codet &code)
const code_assignt & to_code_assign(const codet &code)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::vector< code_assignt > non_null_assignments
optionalt< code_assignt > null_assignment
bool has_suffix(const std::string &s, const std::string &suffix)