Go to the documentation of this file.
32 std::vector<codet> statements;
33 for(
auto sub_expression_it = function_value.
depth_begin();
34 sub_expression_it != function_value.
depth_end();
37 if(sub_expression_it->id() == ID_code)
39 statements.push_back(
to_code(*sub_expression_it));
48 const std::vector<codet>
53 const symbolt *entry_point_function =
55 REQUIRE(entry_point_function !=
nullptr);
73 const std::vector<codet> &statements,
81 for(
const auto &assignment : statements)
83 if(assignment.get_statement() == ID_assign)
87 if(code_assign.
lhs().
id() == ID_member)
91 if(superclass_name.has_value())
105 const irep_idt supercomponent_name =
106 "@" +
id2string(superclass_name.value());
110 ode.
build(superclass_expr, ns);
120 locations.null_assignment = code_assign;
124 locations.non_null_assignments.push_back(code_assign);
138 ode.
build(member_expr, ns);
148 locations.null_assignment = code_assign;
152 locations.non_null_assignments.push_back(code_assign);
170 const std::vector<codet> &statements,
175 for(
const auto &assignment : statements)
177 if(assignment.get_statement() == ID_assign)
181 if(code_assign.
lhs().
id() == ID_member)
186 member_expr.
op().
id() == ID_dereference)
190 pointer.id() == ID_symbol &&
222 const std::vector<codet> &instructions)
224 INFO(
"Looking for symbol: " << pointer_name);
225 std::regex special_chars{R
"([-[\]{}()*+?.,\^$|#\s])"};
226 std::string sanitized =
227 std::regex_replace(id2string(pointer_name), special_chars, R"(\$&)");
229 std::regex(
"^" + sanitized +
"$"), instructions);
234 const std::regex &pointer_name_match,
235 const std::vector<codet> &instructions)
238 bool found_assignment =
false;
239 std::vector<irep_idt> all_symbols;
240 for(
const codet &statement : instructions)
242 if(statement.get_statement() == ID_assign)
245 if(code_assign.
lhs().
id() == ID_symbol)
263 found_assignment =
true;
269 std::ostringstream found_symbols;
270 for(
const auto &entry : all_symbols)
272 found_symbols << entry << std::endl;
274 INFO(
"Symbols: " << found_symbols.str());
275 REQUIRE(found_assignment);
288 const std::vector<codet> &entry_point_instructions)
290 for(
const auto &statement : entry_point_instructions)
292 if(statement.get_statement() == ID_decl)
296 if(decl_statement.get_identifier() == variable_name)
298 return decl_statement;
311 const std::vector<codet> &entry_point_instructions,
315 symbol_identifier, entry_point_instructions)
317 REQUIRE(assignments.size() == 1);
318 return assignments[0].rhs();
330 const std::vector<codet> &entry_point_instructions,
334 entry_point_instructions, symbol_identifier);
336 return expr_try_dynamic_cast<symbol_exprt>(
skip_typecast(expr));
355 const std::vector<codet> &entry_point_instructions,
356 const irep_idt &input_symbol_identifier)
360 entry_point_instructions, input_symbol_identifier);
362 if(symbol_assigned_to_input_symbol)
365 entry_point_instructions,
369 return input_symbol_identifier;
389 const irep_idt &component_type_name,
391 const std::vector<codet> &entry_point_instructions,
398 const auto &component_assignments =
400 entry_point_instructions,
406 "looking for component assignment " << component_name <<
" in "
408 REQUIRE(component_assignments.non_null_assignments.size() == 1);
413 const symbol_exprt *rhs_symbol_expr = expr_try_dynamic_cast<symbol_exprt>(
414 skip_typecast(component_assignments.non_null_assignments[0].rhs()));
415 REQUIRE(rhs_symbol_expr);
424 const auto &component_declaration =
426 symbol_identifier, entry_point_instructions);
427 const typet &component_type =
429 REQUIRE(component_type.
id() == ID_struct_tag);
430 const auto &component_struct =
432 REQUIRE(component_struct.get(ID_name) == component_type_name);
434 return symbol_identifier;
450 const irep_idt &array_component_name,
452 const std::vector<codet> &entry_point_instructions,
457 const auto &component_assignments =
459 entry_point_instructions,
462 array_component_name,
464 REQUIRE(component_assignments.non_null_assignments.size() == 1);
469 const exprt &component_assignment_rhs_expr =
470 component_assignments.non_null_assignments[0].rhs();
475 const auto &component_assignment_rhs =
477 const auto &component_reference_tmp_name =
481 REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
485 .
get(ID_identifier) == array_type_name);
489 const auto &component_reference_assignments =
491 component_reference_tmp_name, entry_point_instructions);
492 REQUIRE(component_reference_assignments.non_null_assignments.size() == 1);
493 const exprt &component_reference_assignment_rhs_expr =
494 component_reference_assignments.non_null_assignments[0].rhs();
497 PRECONDITION(component_reference_assignment_rhs_expr.
id() == ID_side_effect);
498 const auto &array_component_reference_assignment_rhs =
503 array_component_reference_assignment_rhs.type().id() == ID_pointer);
507 REQUIRE(array.
get(ID_identifier) == array_type_name);
509 return component_reference_tmp_name;
520 const std::vector<codet> &entry_point_statements)
528 entry_point_statements);
537 const auto &argument_assignment =
551 const std::vector<codet> &statements,
552 const irep_idt &function_call_identifier)
554 std::vector<code_function_callt> function_calls;
555 for(
const codet &statement : statements)
557 if(statement.get_statement() == ID_function_call)
562 if(function_call.
function().
id() == ID_symbol)
566 function_call_identifier)
568 function_calls.push_back(function_call);
573 return function_calls;
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const char * c_str() const
const typet & subtype() const
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
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...
const code_declt & to_code_decl(const codet &code)
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}.
depth_iteratort depth_begin()
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
The type of an expression, extends irept.
Split an expression into a base object and a (byte) offset.
A codet representing the declaration of a local variable.
std::vector< code_assignt > non_null_assignments
Base class for all expressions.
bool is_java_array_tag(const irep_idt &tag)
See above.
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
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.
side_effect_exprt & to_side_effect_expr(exprt &expr)
Expression to hold a symbol (variable)
bool has_suffix(const std::string &s, const std::string &suffix)
std::vector< codet > get_all_statements(const exprt &function_value)
Expand value of a function to include all child codets.
static const exprt & root_object(const exprt &expr)
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...
const codet & to_code(const exprt &expr)
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...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
codet representation of a function call statement.
The null pointer constant.
const std::string & id2string(const irep_idt &d)
const exprt & compound() const
#define PRECONDITION(CONDITION)
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.
const irep_idt & get_identifier() const
API to expression classes for Pointers.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Utilties for inspecting goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const code_function_callt & to_code_function_call(const codet &code)
nonstd::optional< T > optionalt
optionalt< code_assignt > null_assignment
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.
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.
Extract member of struct or union.
Deprecated expression utility functions.
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, const symbol_tablet &symbol_table)
Checks that the component of the structure (possibly inherited from the superclass) is assigned an ob...
Forward depth-first search iterators These iterators' copy operations are expensive,...
const code_assignt & to_code_assign(const codet &code)
const irep_idt & get(const irep_namet &name) const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Goto Programs with Functions.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
irep_idt get_component_name() const
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...
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
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:
A codet representing an assignment in the program.
depth_iteratort depth_end()
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...
Data structure for representing an arbitrary statement in a program.