require_goto_statements.h File Reference
Utilties for inspecting goto functions. More...
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 | |
| 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: More... | |
| 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}. More... | |
| std::vector< codet > | require_goto_statements::get_all_statements (const exprt &function_value) |
| Expand value of a function to include all child codets. More... | |
| 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. More... | |
| 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. More... | |
| const 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. More... | |
| 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. More... | |
| 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. 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. More... | |
Detailed Description
Utilties for inspecting goto functions.
Definition in file require_goto_statements.h.
