1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
|
/*******************************************************************\
Module: Unit test utilities
Author: Diffblue Ltd.
\*******************************************************************/
/// \file
/// Utilties for inspecting goto functions
#include <goto-programs/goto_instruction_code.h>
#include <regex>
class symbol_table_baset;
#ifndef CPROVER_JAVA_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H
#define CPROVER_JAVA_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H
// NOLINTNEXTLINE(readability/namespace)
namespace require_goto_statements
{
struct pointer_assignment_locationt
{
std::optional<code_assignt> null_assignment;
std::vector<code_assignt> non_null_assignments;
};
class no_decl_found_exceptiont : public std::exception
{
public:
explicit no_decl_found_exceptiont(const std::string &var_name)
: message{"Failed to find declaration for: " + var_name}
{
}
virtual const char *what() const throw()
{
return message.c_str();
}
private:
std::string message;
};
pointer_assignment_locationt find_struct_component_assignments(
const std::vector<codet> &statements,
const irep_idt &structure_name,
const std::optional<irep_idt> &superclass_name,
const irep_idt &component_name,
const symbol_table_baset &symbol_table);
pointer_assignment_locationt find_this_component_assignment(
const std::vector<codet> &statements,
const irep_idt &component_name);
std::vector<codet> get_all_statements(const exprt &function_value);
const std::vector<codet>
require_entry_point_statements(const symbol_table_baset &symbol_table);
pointer_assignment_locationt find_pointer_assignments(
const irep_idt &pointer_name,
const std::vector<codet> &instructions);
pointer_assignment_locationt find_pointer_assignments(
const std::regex &pointer_name_match,
const std::vector<codet> &instructions);
const code_declt &require_declaration_of_name(
const irep_idt &variable_name,
const std::vector<codet> &entry_point_instructions);
irep_idt require_struct_component_assignment(
const irep_idt &structure_name,
const std::optional<irep_idt> &superclass_name,
const irep_idt &component_name,
const irep_idt &component_type_name,
const std::optional<irep_idt> &typecast_name,
const std::vector<codet> &entry_point_instructions,
const symbol_table_baset &symbol_table);
const irep_idt &require_struct_array_component_assignment(
const irep_idt &structure_name,
const std::optional<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_table_baset &symbol_table);
irep_idt require_entry_point_argument_assignment(
const irep_idt &argument_name,
const std::vector<codet> &entry_point_statements);
std::vector<code_function_callt> find_function_calls(
const std::vector<codet> &statements,
const irep_idt &function_call_identifier);
}
#endif // CPROVER_JAVA_TESTING_UTILS_REQUIRE_GOTO_STATEMENTS_H
|
