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 
59  const std::vector<codet> &statements,
60  const irep_idt &component_name);
61 
62 std::vector<codet> get_all_statements(const exprt &function_value);
63 
64 const std::vector<codet>
66 
68  const irep_idt &pointer_name,
69  const std::vector<codet> &instructions);
70 
72  const std::regex &pointer_name_match,
73  const std::vector<codet> &instructions);
74 
76  const irep_idt &variable_name,
77  const std::vector<codet> &entry_point_instructions);
78 
80  const irep_idt &structure_name,
81  const optionalt<irep_idt> &superclass_name,
82  const irep_idt &component_name,
83  const irep_idt &component_type_name,
84  const optionalt<irep_idt> &typecast_name,
85  const std::vector<codet> &entry_point_instructions);
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 irep_idt &array_component_element_type_name,
93  const std::vector<codet> &entry_point_instructions);
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
std::vector< codet > get_all_statements(const exprt &function_value)
Expand value of a function to include all child codets.
const std::vector< codet > require_entry_point_statements(const symbol_tablet &symbol_table)
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)
Checks that the component of the structure (possibly inherited from the superclass) is assigned an ob...
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)
Find assignment statements of the form:
A declaration of a local variable.
Definition: std_code.h:254
nonstd::optional< T > optionalt
Definition: optional.h:35
The symbol table.
Definition: symbol_table.h:19
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...
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
API to type classes.
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 irep_idt &array_component_element_type_name, const std::vector< codet > &entry_point_instructions)
Checks that the array component of the structure (possibly inherited from the superclass) is assigned...
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.
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...
Base class for all expressions.
Definition: expr.h:42
Concrete Goto Program.