19
19
#ifndef CPROVER_TESTING_UTILS_CHECK_GOTO_FUNCTIONS_H
20
20
#define CPROVER_TESTING_UTILS_CHECK_GOTO_FUNCTIONS_H
21
21
22
+ namespace require_goto_statements
23
+ {
24
+ struct pointer_assignment_locationt
25
+ {
26
+ optionalt<code_assignt> null_assignment;
27
+ std::vector<code_assignt> non_null_assignments;
28
+ };
29
+
22
30
class no_decl_found_exception : public std ::exception
23
31
{
24
32
public:
@@ -38,26 +46,18 @@ class no_decl_found_exception : public std::exception
38
46
std::string _varname;
39
47
};
40
48
41
- namespace require_goto_statements
42
- {
43
49
std::vector<code_assignt> find_struct_component_assignments (
44
50
const std::vector<codet> &statements,
45
51
const irep_idt &structure_name,
46
52
const irep_idt &component_name);
47
53
48
- struct pointer_assignment_locationt
49
- {
50
- optionalt<code_assignt> null_assignment;
51
- std::vector<code_assignt> non_null_assignments;
52
- };
53
-
54
54
std::vector<codet> get_all_statements (const exprt &function_value);
55
55
56
56
pointer_assignment_locationt find_pointer_assignments (
57
57
const irep_idt &pointer_name,
58
58
const std::vector<codet> &instructions);
59
59
60
- const code_declt &find_declaration_by_name (
60
+ const code_declt &require_declaration_of_name (
61
61
const irep_idt &variable_name,
62
62
const std::vector<codet> &entry_point_instructions);
63
63
}
0 commit comments