Go to the documentation of this file.
28 std::vector<codet> statements;
29 for(
auto sub_expression_it = function_value.
depth_begin();
30 sub_expression_it != function_value.
depth_end();
33 if(sub_expression_it->id() == ID_code)
35 statements.push_back(
to_code(*sub_expression_it));
44 const std::vector<codet>
49 const symbolt *entry_point_function =
51 REQUIRE(entry_point_function !=
nullptr);
69 const std::vector<codet> &statements,
77 for(
const auto &assignment : statements)
79 if(assignment.get_statement() == ID_assign)
83 if(code_assign.
lhs().
id() == ID_member)
87 if(superclass_name.has_value())
101 const irep_idt supercomponent_name =
102 "@" +
id2string(superclass_name.value());
106 ode.
build(superclass_expr, ns);
116 locations.null_assignment = code_assign;
120 locations.non_null_assignments.push_back(code_assign);
134 ode.
build(member_expr, ns);
144 locations.null_assignment = code_assign;
148 locations.non_null_assignments.push_back(code_assign);
166 const std::vector<codet> &statements,
171 for(
const auto &assignment : statements)
173 if(assignment.get_statement() == ID_assign)
177 if(code_assign.
lhs().
id() == ID_member)
182 member_expr.
op().
id() == ID_dereference)
186 pointer.id() == ID_symbol &&
218 const std::vector<codet> &instructions)
220 INFO(
"Looking for symbol: " << pointer_name);
221 std::regex special_chars{R
"([-[\]{}()*+?.,\^$|#\s])"};
222 std::string sanitized =
223 std::regex_replace(id2string(pointer_name), special_chars, R"(\$&)");
225 std::regex(
"^" + sanitized +
"$"), instructions);
230 const std::regex &pointer_name_match,
231 const std::vector<codet> &instructions)
234 bool found_assignment =
false;
235 std::vector<irep_idt> all_symbols;
236 for(
const codet &statement : instructions)
238 if(statement.get_statement() == ID_assign)
241 if(code_assign.
lhs().
id() == ID_symbol)
259 found_assignment =
true;
265 std::ostringstream found_symbols;
266 for(
const auto &entry : all_symbols)
268 found_symbols << entry << std::endl;
270 INFO(
"Symbols: " << found_symbols.str());
271 REQUIRE(found_assignment);
284 const std::vector<codet> &entry_point_instructions)
286 for(
const auto &statement : entry_point_instructions)
288 if(statement.get_statement() == ID_decl)
292 if(decl_statement.get_identifier() == variable_name)
294 return decl_statement;
307 const std::vector<codet> &entry_point_instructions,
311 symbol_identifier, entry_point_instructions)
313 REQUIRE(assignments.size() == 1);
314 return assignments[0].rhs();
326 const std::vector<codet> &entry_point_instructions,
330 entry_point_instructions, symbol_identifier);
332 return expr_try_dynamic_cast<symbol_exprt>(
skip_typecast(expr));
351 const std::vector<codet> &entry_point_instructions,
352 const irep_idt &input_symbol_identifier)
356 entry_point_instructions, input_symbol_identifier);
358 if(symbol_assigned_to_input_symbol)
361 entry_point_instructions,
365 return input_symbol_identifier;
385 const irep_idt &component_type_name,
387 const std::vector<codet> &entry_point_instructions,
394 const auto &component_assignments =
396 entry_point_instructions,
402 "looking for component assignment " << component_name <<
" in "
404 REQUIRE(component_assignments.non_null_assignments.size() == 1);
409 const symbol_exprt *rhs_symbol_expr = expr_try_dynamic_cast<symbol_exprt>(
410 skip_typecast(component_assignments.non_null_assignments[0].rhs()));
411 REQUIRE(rhs_symbol_expr);
420 const auto &component_declaration =
422 symbol_identifier, entry_point_instructions);
423 const typet &component_type =
425 REQUIRE(component_type.
id() == ID_struct_tag);
426 const auto &component_struct =
428 REQUIRE(component_struct.get(ID_name) == component_type_name);
430 return symbol_identifier;
446 const irep_idt &array_component_name,
448 const std::vector<codet> &entry_point_instructions,
453 const auto &component_assignments =
455 entry_point_instructions,
458 array_component_name,
460 REQUIRE(component_assignments.non_null_assignments.size() == 1);
465 const exprt &component_assignment_rhs_expr =
466 component_assignments.non_null_assignments[0].rhs();
471 const auto &component_assignment_rhs =
473 const auto &component_reference_tmp_name =
477 REQUIRE(component_assignment_rhs.type().id() == ID_pointer);
481 .
get(ID_identifier) == array_type_name);
485 const auto &component_reference_assignments =
487 component_reference_tmp_name, entry_point_instructions);
488 REQUIRE(component_reference_assignments.non_null_assignments.size() == 1);
489 const exprt &component_reference_assignment_rhs_expr =
490 component_reference_assignments.non_null_assignments[0].rhs();
493 PRECONDITION(component_reference_assignment_rhs_expr.
id() == ID_side_effect);
494 const auto &array_component_reference_assignment_rhs =
499 array_component_reference_assignment_rhs.type().id() == ID_pointer);
503 REQUIRE(array.
get(ID_identifier) == array_type_name);
505 return component_reference_tmp_name;
516 const std::vector<codet> &entry_point_statements)
524 entry_point_statements);
533 const auto &argument_assignment =
547 const std::vector<codet> &statements,
548 const irep_idt &function_call_identifier)
550 std::vector<code_function_callt> function_calls;
551 for(
const codet &statement : statements)
553 if(statement.get_statement() == ID_function_call)
558 if(function_call.
function().
id() == ID_symbol)
562 function_call_identifier)
564 function_calls.push_back(function_call);
569 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()
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.
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
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)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const exprt & root_object() const
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.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
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.