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/irep.h>
13 #include <util/expr.h>
14 #include <util/optional.h>
15 #include <util/std_code.h>
16 #include <util/std_types.h>
18 
19 #include <regex>
20 
21 #ifndef CPROVER_JAVA_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H
22 #define CPROVER_JAVA_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H
23 
24 // NOLINTNEXTLINE(readability/namespace)
26 {
28 {
30  std::vector<code_assignt> non_null_assignments;
31 };
32 
33 class no_decl_found_exceptiont : public std::exception
34 {
35 public:
36  explicit no_decl_found_exceptiont(const std::string &var_name)
37  : _varname(var_name)
38  {
39  }
40 
41  virtual const char *what() const throw()
42  {
43  std::ostringstream stringStream;
44  stringStream << "Failed to find declaration for: " << _varname;
45  return stringStream.str().c_str();
46  }
47 
48 private:
49  std::string _varname;
50 };
51 
53  const std::vector<codet> &statements,
54  const irep_idt &structure_name,
55  const optionalt<irep_idt> &superclass_name,
56  const irep_idt &component_name,
57  const symbol_tablet &symbol_table);
58 
60  const std::vector<codet> &statements,
61  const irep_idt &component_name);
62 
63 std::vector<codet> get_all_statements(const exprt &function_value);
64 
65 const std::vector<codet>
67 
69  const irep_idt &pointer_name,
70  const std::vector<codet> &instructions);
71 
73  const std::regex &pointer_name_match,
74  const std::vector<codet> &instructions);
75 
77  const irep_idt &variable_name,
78  const std::vector<codet> &entry_point_instructions);
79 
81  const irep_idt &structure_name,
82  const optionalt<irep_idt> &superclass_name,
83  const irep_idt &component_name,
84  const irep_idt &component_type_name,
85  const optionalt<irep_idt> &typecast_name,
86  const std::vector<codet> &entry_point_instructions,
87  const symbol_tablet &symbol_table);
88 
90  const irep_idt &structure_name,
91  const optionalt<irep_idt> &superclass_name,
92  const irep_idt &array_component_name,
93  const irep_idt &array_type_name,
94  const std::vector<codet> &entry_point_instructions,
95  const symbol_tablet &symbol_table);
96 
98  const irep_idt &argument_name,
99  const std::vector<codet> &entry_point_statements);
100 
101 std::vector<code_function_callt> find_function_calls(
102  const std::vector<codet> &statements,
103  const irep_idt &function_call_identifier);
104 }
105 
106 #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:35
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
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:43
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:159
optional.h
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:352
require_goto_statements::pointer_assignment_locationt::non_null_assignments
std::vector< code_assignt > non_null_assignments
Definition: require_goto_statements.h:30
exprt
Base class for all expressions.
Definition: expr.h:54
require_goto_statements
Definition: require_goto_statements.h:25
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:272
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:36
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:24
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:461
expr.h
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:494
require_goto_statements::no_decl_found_exceptiont::_varname
std::string _varname
Definition: require_goto_statements.h:49
require_goto_statements::pointer_assignment_locationt
Definition: require_goto_statements.h:27
std_types.h
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:29
goto_program.h
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:206
require_goto_statements::no_decl_found_exceptiont::what
virtual const char * what() const
Definition: require_goto_statements.h:41
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:302
require_goto_statements::no_decl_found_exceptiont
Definition: require_goto_statements.h:33
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:390
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:66
irep.h