21 #ifndef CPROVER_JAVA_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H 22 #define CPROVER_JAVA_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H 41 virtual const char *
what()
const throw()
43 std::ostringstream stringStream;
44 stringStream <<
"Failed to find declaration for: " <<
_varname;
45 return stringStream.str().c_str();
53 const std::vector<codet> &statements,
59 const std::vector<codet> &statements,
64 const std::vector<codet>
69 const std::vector<codet> &instructions);
72 const std::regex &pointer_name_match,
73 const std::vector<codet> &instructions);
77 const std::vector<codet> &entry_point_instructions);
85 const std::vector<codet> &entry_point_instructions);
90 const irep_idt &array_component_name,
92 const irep_idt &array_component_element_type_name,
93 const std::vector<codet> &entry_point_instructions);
97 const std::vector<codet> &entry_point_statements);
100 const std::vector<codet> &statements,
101 const irep_idt &function_call_identifier);
104 #endif // CPROVER_JAVA_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H std::vector< codet > get_all_statements(const exprt &function_value)
Expand value of a function to include all child codets.
const std::vector< codet > require_entry_point_statements(const symbol_tablet &symbol_table)
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...
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)
Find assignment statements of the form:
A declaration of a local variable.
nonstd::optional< T > optionalt
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 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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
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...
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.
no_decl_found_exceptiont(const std::string &var_name)
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.
optionalt< code_assignt > null_assignment
virtual const char * what() const