cprover
|
Classes | |
class | no_decl_found_exceptiont |
struct | pointer_assignment_locationt |
Functions | |
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: More... | |
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}. More... | |
std::vector< codet > | get_all_statements (const exprt &function_value) |
Expand value of a function to include all child codets. More... | |
const std::vector< codet > | require_entry_point_statements (const symbol_tablet &symbol_table) |
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. More... | |
pointer_assignment_locationt | find_pointer_assignments (const std::regex &pointer_name_match, const std::vector< codet > &instructions) |
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. More... | |
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 object of the given type. More... | |
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 an array with given element type. More... | |
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 object in the entry point function. More... | |
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 matches the provided identifier. More... | |
std::vector< code_function_callt > require_goto_statements::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 matches the provided identifier.
statements | The collection of statements to inspect |
function_call_identifier | The symbol identifier of the function that should have been called |
Definition at line 483 of file require_goto_statements.cpp.
References code_function_callt::function(), irept::id(), to_code_function_call(), and to_symbol_expr().
require_goto_statements::pointer_assignment_locationt require_goto_statements::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.
pointer_name | The name of the variable |
instructions | The instructions to look through |
Definition at line 200 of file require_goto_statements.cpp.
References id2string().
Referenced by require_entry_point_argument_assignment(), require_struct_array_component_assignment(), and require_struct_component_assignment().
require_goto_statements::pointer_assignment_locationt require_goto_statements::find_pointer_assignments | ( | const std::regex & | pointer_name_match, |
const std::vector< codet > & | instructions | ||
) |
Definition at line 213 of file require_goto_statements.cpp.
References symbol_exprt::get_identifier(), irept::id(), id2string(), code_assignt::lhs(), require_goto_statements::pointer_assignment_locationt::non_null_assignments, require_goto_statements::pointer_assignment_locationt::null_assignment, code_assignt::rhs(), to_code_assign(), to_pointer_type(), to_symbol_expr(), and exprt::type().
require_goto_statements::pointer_assignment_locationt require_goto_statements::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:
structure_name
.\p superclass_name.component_name
= (if it's a component inherited from the superclass)structure_name
.component_name
= (otherwise) statements | The statements to look through |
structure_name | The name of variable of type struct |
superclass_name | The name of the superclass (if given) |
component_name | The name of the component of the superclass that should be assigned |
Definition at line 65 of file require_goto_statements.cpp.
References member_exprt::compound(), member_exprt::get_component_name(), symbol_exprt::get_identifier(), irept::id(), id2string(), code_assignt::lhs(), require_goto_statements::pointer_assignment_locationt::non_null_assignments, require_goto_statements::pointer_assignment_locationt::null_assignment, unary_exprt::op(), exprt::op0(), code_assignt::rhs(), member_exprt::symbol(), to_code_assign(), to_member_expr(), to_pointer_type(), and exprt::type().
Referenced by require_struct_array_component_assignment(), and require_struct_component_assignment().
require_goto_statements::pointer_assignment_locationt require_goto_statements::find_this_component_assignment | ( | const std::vector< codet > & | statements, |
const irep_idt & | component_name | ||
) |
Find assignment statements that set this->{component_name}.
statements | The statements to look through |
component_name | The name of the component whose assignments we are looking for. |
Definition at line 153 of file require_goto_statements.cpp.
References member_exprt::get_component_name(), has_suffix(), irept::id(), id2string(), code_assignt::lhs(), require_goto_statements::pointer_assignment_locationt::non_null_assignments, require_goto_statements::pointer_assignment_locationt::null_assignment, unary_exprt::op(), exprt::op0(), code_assignt::rhs(), to_code_assign(), to_member_expr(), to_pointer_type(), to_symbol_expr(), and exprt::type().
Expand value of a function to include all child codets.
function_value | The value of the function (e.g. got by looking up the function in the symbol table and getting the value) |
function_value
Definition at line 24 of file require_goto_statements.cpp.
References exprt::depth_begin(), exprt::depth_end(), and to_code().
Referenced by require_entry_point_statements().
const code_declt & require_goto_statements::require_declaration_of_name | ( | const irep_idt & | variable_name, |
const std::vector< codet > & | entry_point_instructions | ||
) |
Find the declaration of the specific variable.
variable_name | The name of the variable. |
entry_point_instructions | The statements to look through |
no_decl_found_exceptiont | if no declaration of the specific variable is found |
Definition at line 266 of file require_goto_statements.cpp.
References dstringt::c_str(), and to_code_decl().
Referenced by require_struct_component_assignment().
const irep_idt & require_goto_statements::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 object in the entry point function.
argument_name | Name of the input argument of method under test |
entry_point_statements | The statements to look through |
Definition at line 450 of file require_goto_statements.cpp.
References goto_functionst::entry_point(), find_pointer_assignments(), id2string(), require_goto_statements::pointer_assignment_locationt::non_null_assignments, to_address_of_expr(), and to_symbol_expr().
const std::vector< codet > require_goto_statements::require_entry_point_statements | ( | const symbol_tablet & | symbol_table | ) |
symbol_table | Symbol table for the test |
Definition at line 43 of file require_goto_statements.cpp.
References goto_functionst::entry_point(), get_all_statements(), symbol_table_baset::lookup(), and symbolt::value.
const irep_idt & require_goto_statements::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 an array with given element type.
structure_name | The name the variable |
superclass_name | The name of its superclass (if given) |
array_component_name | The name of the array field of the superclass |
array_type_name | The type of the array, e.g., java::array[reference] |
array_component_element_type_name | The element type of the array |
entry_point_instructions | The statements to look through |
Definition at line 381 of file require_goto_statements.cpp.
References find_pointer_assignments(), find_struct_component_assignments(), is_java_array_tag(), PRECONDITION, to_pointer_type(), to_side_effect_expr(), to_symbol_expr(), to_symbol_type(), and to_typecast_expr().
const irep_idt & require_goto_statements::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 object of the given type.
structure_name | The name the variable |
superclass_name | The name of its superclass (if given) |
component_name | The name of the field of the superclass |
component_type_name | The name of the required type of the field |
typecast_name | The name of the type to which the object is cast (if there is a typecast) |
entry_point_instructions | The statements to look through |
Definition at line 295 of file require_goto_statements.cpp.
References find_pointer_assignments(), find_struct_component_assignments(), require_goto_statements::pointer_assignment_locationt::non_null_assignments, require_declaration_of_name(), to_address_of_expr(), to_pointer_type(), to_struct_type(), to_symbol_expr(), to_symbol_type(), and to_typecast_expr().