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