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, const symbol_tablet &symbol_table)
	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, const symbol_tablet &symbol_table)
	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 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 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 550 of file require_goto_statements.cpp.

◆ 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 219 of file require_goto_statements.cpp.

◆ 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 232 of file require_goto_statements.cpp.

◆ 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,
		const symbol_tablet &	symbol_table
	)

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
symbol_table	A symbol table to enable type lookups should be assigned

Returns: All the assignments to that component.

Definition at line 71 of file require_goto_statements.cpp.

◆ 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 168 of file require_goto_statements.cpp.

◆ 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 29 of file require_goto_statements.cpp.

◆ 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 285 of file require_goto_statements.cpp.

◆ 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 518 of file require_goto_statements.cpp.

◆ 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 48 of file require_goto_statements.cpp.

◆ 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 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 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]
entry_point_instructions	The statements to look through
symbol_table	A symbol table to enable type lookups

Returns: The identifier of the variable assigned to the field

Definition at line 446 of file require_goto_statements.cpp.

◆ 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,
		const symbol_tablet &	symbol_table
	)

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
symbol_table	A symbol table to enable type lookups

Returns: The identifier of the ultimate source symbol assigned to the field, which will be used for future calls to require_struct_component_assignment.

Definition at line 384 of file require_goto_statements.cpp.

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