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

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

statements	The collection of statements to inspect
function_call_identifier	The 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_name	The name of the variable
instructions	The 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]

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

◆ 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

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

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

statements	The statements to look through
component_name	The 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_value The 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_name	The name of the variable.
entry_point_instructions	The statements to look through

Returns: The declaration statement corresponding to that variable

Exceptions

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

◆ 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_name	Name of the input argument of method under test
entry_point_statements	The 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_table Symbol 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_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

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_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

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

Classes

Functions

Function Documentation

◆ find_function_calls()

◆ find_pointer_assignments() [1/2]

◆ find_pointer_assignments() [2/2]

◆ find_struct_component_assignments()

◆ find_this_component_assignment()

◆ get_all_statements()

◆ require_declaration_of_name()

◆ require_entry_point_argument_assignment()

◆ require_entry_point_statements()

◆ require_struct_array_component_assignment()

◆ require_struct_component_assignment()