cprover
require_goto_statements Namespace Reference

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< codetget_all_statements (const exprt &function_value)
 Expand value of a function to include all child codets. More...
 
const std::vector< codetrequire_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_decltrequire_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_idtrequire_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_idtrequire_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_idtrequire_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_calltfind_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...
 

Function Documentation

◆ find_function_calls()

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.

Parameters
statementsThe collection of statements to inspect
function_call_identifierThe symbol identifier of the function that should have been called
Returns
All calls to the matching function inside the statements

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().

◆ find_pointer_assignments() [1/2]

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.

Parameters
pointer_nameThe name of the variable
instructionsThe instructions to look through
Returns
: A structure that contains the null assignment if found, and a vector of all other assignments

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().

◆ find_pointer_assignments() [2/2]

◆ find_struct_component_assignments()

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)
    Parameters
    statementsThe statements to look through
    structure_nameThe name of variable of type struct
    superclass_nameThe name of the superclass (if given)
    component_nameThe name of the component of the superclass that should be assigned
    Returns
    : All the assignments to that component.

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().

◆ find_this_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}.

Parameters
statementsThe statements to look through
component_nameThe name of the component whose assignments we are looking for.
Returns
A collection of all non-null assignments to this component and, if present, a null assignment.

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().

◆ get_all_statements()

std::vector< codet > require_goto_statements::get_all_statements ( const exprt function_value)

Expand value of a function to include all child codets.

Parameters
function_valueThe value of the function (e.g. got by looking up the function in the symbol table and getting the value)
Returns
: All ID_code statements in the tree rooted at 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().

◆ require_declaration_of_name()

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.

Parameters
variable_nameThe name of the variable.
entry_point_instructionsThe statements to look through
Returns
The declaration statement corresponding to that variable
Exceptions
no_decl_found_exceptiontif 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().

◆ require_entry_point_argument_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.

Parameters
argument_nameName of the input argument of method under test
entry_point_statementsThe statements to look through
Returns
The identifier of the variable assigned to the input argument

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().

◆ require_entry_point_statements()

const std::vector< codet > require_goto_statements::require_entry_point_statements ( const symbol_tablet symbol_table)
Parameters
symbol_tableSymbol table for the test
Returns
All codet statements of the __CPROVER_start function

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.

◆ require_struct_array_component_assignment()

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.

Parameters
structure_nameThe name the variable
superclass_nameThe name of its superclass (if given)
array_component_nameThe name of the array field of the superclass
array_type_nameThe type of the array, e.g., java::array[reference]
array_component_element_type_nameThe element type of the array
entry_point_instructionsThe statements to look through
Returns
The identifier of the variable assigned to the field

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().

◆ require_struct_component_assignment()

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.

Parameters
structure_nameThe name the variable
superclass_nameThe name of its superclass (if given)
component_nameThe name of the field of the superclass
component_type_nameThe name of the required type of the field
typecast_nameThe name of the type to which the object is cast (if there is a typecast)
entry_point_instructionsThe statements to look through
Returns
The identifier of the variable assigned to the field

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().