|
19 | 19 | #ifndef CPROVER_TESTING_UTILS_CHECK_GOTO_FUNCTIONS_H |
20 | 20 | #define CPROVER_TESTING_UTILS_CHECK_GOTO_FUNCTIONS_H |
21 | 21 |
|
22 | | -class no_decl_found_exception : public std::exception |
23 | | -{ |
24 | | -public: |
25 | | - explicit no_decl_found_exception(const std::string &varname) : _varname |
26 | | - (varname) {} |
27 | | - |
28 | | - virtual const char *what() const throw() { |
29 | | - std::ostringstream stringStream; |
30 | | - stringStream << "Failed to find declaration for: " |
31 | | - << _varname; |
32 | | - return stringStream.str().c_str(); |
33 | | - } |
34 | | - |
35 | | -private: |
36 | | - std::string _varname; |
37 | | -}; |
38 | 22 |
|
39 | 23 | namespace require_goto_statements |
40 | 24 | { |
41 | | - std::vector<code_assignt> find_struct_component_assignments( |
42 | | - const std::vector<codet> &statements, |
43 | | - const irep_idt &structure_name, |
44 | | - const irep_idt &component_name); |
45 | | - |
46 | 25 | struct pointer_assignment_locationt |
47 | 26 | { |
48 | 27 | optionalt<code_assignt> null_assignment; |
49 | 28 | std::vector<code_assignt> non_null_assignments; |
50 | 29 | }; |
51 | 30 |
|
| 31 | + class no_decl_found_exception : public std::exception |
| 32 | + { |
| 33 | + public: |
| 34 | + explicit no_decl_found_exception(const std::string &varname) : _varname |
| 35 | + (varname) {} |
| 36 | + |
| 37 | + virtual const char *what() const throw() { |
| 38 | + std::ostringstream stringStream; |
| 39 | + stringStream << "Failed to find declaration for: " |
| 40 | + << _varname; |
| 41 | + return stringStream.str().c_str(); |
| 42 | + } |
| 43 | + |
| 44 | + private: |
| 45 | + std::string _varname; |
| 46 | + }; |
| 47 | + |
| 48 | + std::vector<code_assignt> find_struct_component_assignments( |
| 49 | + const std::vector<codet> &statements, |
| 50 | + const irep_idt &structure_name, |
| 51 | + const irep_idt &component_name); |
| 52 | + |
52 | 53 | std::vector<codet> get_all_statements(const exprt &function_value); |
53 | 54 |
|
54 | 55 | pointer_assignment_locationt find_pointer_assignments( |
55 | 56 | const irep_idt &pointer_name, |
56 | 57 | const std::vector<codet> &instructions); |
57 | 58 |
|
58 | | - const code_declt & find_declaration_by_name( |
| 59 | + const code_declt &require_declaration_of_name( |
59 | 60 | const irep_idt &variable_name, |
60 | 61 | const std::vector<codet> &entry_point_instructions); |
61 | 62 | } |
|
0 commit comments