File tree Expand file tree Collapse file tree 3 files changed +20
-7
lines changed Expand file tree Collapse file tree 3 files changed +20
-7
lines changed Original file line number Diff line number Diff line change @@ -21,7 +21,6 @@ Date: December 2016
21
21
#include < util/cprover_prefix.h>
22
22
#include < util/prefix.h>
23
23
24
- #include < util/exception_utils.h>
25
24
#include < util/invariant.h>
26
25
27
26
#include < goto-programs/goto_functions.h>
@@ -36,7 +35,7 @@ void slice_global_inits(goto_modelt &goto_model)
36
35
goto_functionst &goto_functions=goto_model.goto_functions ;
37
36
38
37
if (goto_functions.function_map .count (entry_point) == 0 )
39
- throw incorrect_goto_program_exceptiont (" entry point not found" );
38
+ throw user_input_error_exceptiont (" entry point not found" );
40
39
41
40
// Get the call graph restricted to functions reachable from
42
41
// the entry point:
Original file line number Diff line number Diff line change @@ -14,8 +14,27 @@ Date: December 2016
14
14
#ifndef CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H
15
15
#define CPROVER_GOTO_PROGRAMS_SLICE_GLOBAL_INITS_H
16
16
17
+ #include < util/exception_utils.h>
18
+
17
19
class goto_modelt ;
18
20
21
+ class user_input_error_exceptiont : public cprover_exception_baset
22
+ {
23
+ public:
24
+ explicit user_input_error_exceptiont (std::string message)
25
+ : message(std::move(message))
26
+ {
27
+ }
28
+
29
+ std::string what () const
30
+ {
31
+ return message;
32
+ }
33
+
34
+ private:
35
+ std::string message;
36
+ };
37
+
19
38
void slice_global_inits (goto_modelt &);
20
39
21
40
#endif
Original file line number Diff line number Diff line change @@ -76,11 +76,6 @@ int parse_options_baset::main()
76
76
std::cerr << e.what () << " \n " ;
77
77
return CPROVER_EXIT_USAGE_ERROR;
78
78
}
79
- catch (const incorrect_goto_program_exceptiont &e)
80
- {
81
- std::cerr << e.what () << " \n " ;
82
- return CPROVER_EXIT_INTERNAL_ERROR;
83
- }
84
79
catch (const cprover_exception_baset &e)
85
80
{
86
81
std::cerr << e.what () << ' \n ' ;
You can’t perform that action at this time.
0 commit comments