require_goto_statements.h File Reference

Utilties for inspecting goto functions. More...

#include <goto-programs/goto_instruction_code.h>
#include <regex>

Include dependency graph for require_goto_statements.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	require_goto_statements::pointer_assignment_locationt
class	require_goto_statements::no_decl_found_exceptiont

Namespaces
namespace	require_goto_statements

Functions
pointer_assignment_locationt	require_goto_statements::find_struct_component_assignments (const std::vector< codet > &statements, const irep_idt &structure_name, const std::optional< irep_idt > &superclass_name, const irep_idt &component_name, const symbol_table_baset &symbol_table)
	Find assignment statements of the form:
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}.
std::vector< codet >	require_goto_statements::get_all_statements (const exprt &function_value)
	Expand value of a function to include all child codets.
const std::vector< codet >	require_goto_statements::require_entry_point_statements (const symbol_table_baset &symbol_table)
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_assignment_locationt	require_goto_statements::find_pointer_assignments (const std::regex &pointer_name_match, const std::vector< codet > &instructions)
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.
irep_idt	require_goto_statements::require_struct_component_assignment (const irep_idt &structure_name, const std::optional< irep_idt > &superclass_name, const irep_idt &component_name, const irep_idt &component_type_name, const std::optional< irep_idt > &typecast_name, const std::vector< codet > &entry_point_instructions, const symbol_table_baset &symbol_table)
	Checks that the component of the structure (possibly inherited from the superclass) is assigned an object of the given type.
const irep_idt &	require_goto_statements::require_struct_array_component_assignment (const irep_idt &structure_name, const std::optional< 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_table_baset &symbol_table)
	Checks that the array component of the structure (possibly inherited from the superclass) is assigned an array with given element type.
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.
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.

Detailed Description

Utilties for inspecting goto functions.

Definition in file require_goto_statements.h.