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  : message{"Failed to find declaration for: " + var_name}
38  {
39  }
40 
41  virtual const char *what() const throw()
42  {
43  return message.c_str();
44  }
45 
46 private:
47  std::string message;
48 };
49 
51  const std::vector<codet> &statements,
52  const irep_idt &structure_name,
53  const optionalt<irep_idt> &superclass_name,
54  const irep_idt &component_name,
55  const symbol_tablet &symbol_table);
56 
58  const std::vector<codet> &statements,
59  const irep_idt &component_name);
60 
61 std::vector<codet> get_all_statements(const exprt &function_value);
62 
63 const std::vector<codet>
65 
67  const irep_idt &pointer_name,
68  const std::vector<codet> &instructions);
69 
71  const std::regex &pointer_name_match,
72  const std::vector<codet> &instructions);
73 
75  const irep_idt &variable_name,
76  const std::vector<codet> &entry_point_instructions);
77 
79  const irep_idt &structure_name,
80  const optionalt<irep_idt> &superclass_name,
81  const irep_idt &component_name,
82  const irep_idt &component_type_name,
83  const optionalt<irep_idt> &typecast_name,
84  const std::vector<codet> &entry_point_instructions,
85  const symbol_tablet &symbol_table);
86 
88  const irep_idt &structure_name,
89  const optionalt<irep_idt> &superclass_name,
90  const irep_idt &array_component_name,
91  const irep_idt &array_type_name,
92  const std::vector<codet> &entry_point_instructions,
93  const symbol_tablet &symbol_table);
94 
96  const irep_idt &argument_name,
97  const std::vector<codet> &entry_point_statements);
98 
99 std::vector<code_function_callt> find_function_calls(
100  const std::vector<codet> &statements,
101  const irep_idt &function_call_identifier);
102 }
103 
104 #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:20
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:45
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:165
optional.h
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:402
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:53
require_goto_statements
Definition: require_goto_statements.h:26
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:282
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:26
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:514
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:546
require_goto_statements::pointer_assignment_locationt
Definition: require_goto_statements.h:28
std_types.h
Pre-defined types.
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
Concrete Goto Program.
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:216
require_goto_statements::no_decl_found_exceptiont::what
virtual const char * what() const
Definition: require_goto_statements.h:41
require_goto_statements::no_decl_found_exceptiont::message
std::string message
Definition: require_goto_statements.h:47
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:381
require_goto_statements::no_decl_found_exceptiont
Definition: require_goto_statements.h:34
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:443
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:68
irep.h