cprover
Loading...
Searching...
No Matches
require_goto_statements.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Unit test utilities
4
5Author: Diffblue Ltd.
6
7\*******************************************************************/
8
11
13
14#include <util/optional.h>
15
16#include <regex>
17
18class symbol_tablet;
19
20#ifndef CPROVER_JAVA_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H
21#define CPROVER_JAVA_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H
22
23// NOLINTNEXTLINE(readability/namespace)
25{
27{
29 std::vector<code_assignt> non_null_assignments;
30};
31
32class no_decl_found_exceptiont : public std::exception
33{
34public:
35 explicit no_decl_found_exceptiont(const std::string &var_name)
36 : message{"Failed to find declaration for: " + var_name}
37 {
38 }
39
40 virtual const char *what() const throw()
41 {
42 return message.c_str();
43 }
44
45private:
46 std::string message;
47};
48
50 const std::vector<codet> &statements,
51 const irep_idt &structure_name,
52 const optionalt<irep_idt> &superclass_name,
53 const irep_idt &component_name,
54 const symbol_tablet &symbol_table);
55
57 const std::vector<codet> &statements,
58 const irep_idt &component_name);
59
60std::vector<codet> get_all_statements(const exprt &function_value);
61
62const std::vector<codet>
64
66 const irep_idt &pointer_name,
67 const std::vector<codet> &instructions);
68
70 const std::regex &pointer_name_match,
71 const std::vector<codet> &instructions);
72
74 const irep_idt &variable_name,
75 const std::vector<codet> &entry_point_instructions);
76
78 const irep_idt &structure_name,
79 const optionalt<irep_idt> &superclass_name,
80 const irep_idt &component_name,
81 const irep_idt &component_type_name,
82 const optionalt<irep_idt> &typecast_name,
83 const std::vector<codet> &entry_point_instructions,
84 const symbol_tablet &symbol_table);
85
87 const irep_idt &structure_name,
88 const optionalt<irep_idt> &superclass_name,
89 const irep_idt &array_component_name,
90 const irep_idt &array_type_name,
91 const std::vector<codet> &entry_point_instructions,
92 const symbol_tablet &symbol_table);
93
95 const irep_idt &argument_name,
96 const std::vector<codet> &entry_point_statements);
97
98std::vector<code_function_callt> find_function_calls(
99 const std::vector<codet> &statements,
100 const irep_idt &function_call_identifier);
101}
102
103#endif // CPROVER_JAVA_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H
A codet representing the declaration of a local variable.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
The symbol table.
Definition: symbol_table.h:14
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...
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...
std::vector< codet > get_all_statements(const exprt &function_value)
Expand value of a function to include all child codets.
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 ob...
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 o...
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.
const std::vector< codet > require_entry_point_statements(const symbol_tablet &symbol_table)
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}.
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:
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.
nonstd::optional< T > optionalt
Definition: optional.h:35