File tree 7 files changed +33
-12
lines changed 7 files changed +33
-12
lines changed Original file line number Diff line number Diff line change @@ -319,7 +319,7 @@ void java_bytecode_languaget::initialize_class_loader()
319
319
320
320
static void throwMainClassLoadingError (const std::string &main_class)
321
321
{
322
- throw invalid_source_file_exceptiont (
322
+ throw system_exceptiont (
323
323
" Error: Could not find or load main class " + main_class);
324
324
}
325
325
@@ -393,8 +393,7 @@ bool java_bytecode_languaget::parse(
393
393
std::ifstream jar_file (path);
394
394
if (!jar_file.good ())
395
395
{
396
- throw invalid_source_file_exceptiont (
397
- " Error: Unable to access jarfile " + path);
396
+ throw system_exceptiont (" Error: Unable to access jarfile " + path);
398
397
}
399
398
400
399
// build an object to potentially limit which classes are loaded
Original file line number Diff line number Diff line change @@ -151,14 +151,14 @@ void lazy_goto_modelt::initialize(
151
151
152
152
if (dynamic_cast <java_bytecode_languaget &>(language).parse ())
153
153
{
154
- throw invalid_source_file_exceptiont (" PARSING ERROR" );
154
+ throw invalid_input_exceptiont (" PARSING ERROR" );
155
155
}
156
156
157
157
msg.status () << " Converting" << messaget::eom;
158
158
159
159
if (language_files.typecheck (symbol_table))
160
160
{
161
- throw invalid_source_file_exceptiont (" CONVERSION ERROR" );
161
+ throw invalid_input_exceptiont (" CONVERSION ERROR" );
162
162
}
163
163
}
164
164
else
Original file line number Diff line number Diff line change @@ -181,7 +181,7 @@ void link_goto_model(
181
181
182
182
if (linking.typecheck_main ())
183
183
{
184
- throw invalid_source_file_exceptiont (" typechecking main failed" );
184
+ throw invalid_input_exceptiont (" typechecking main failed" );
185
185
}
186
186
if (link_functions (
187
187
dest.symbol_table ,
@@ -192,6 +192,6 @@ void link_goto_model(
192
192
weak_symbols,
193
193
linking.object_type_updates ))
194
194
{
195
- throw invalid_source_file_exceptiont (" linking failed" );
195
+ throw invalid_input_exceptiont (" linking failed" );
196
196
}
197
197
}
Original file line number Diff line number Diff line change @@ -339,7 +339,7 @@ exprt gdb_value_extractort::get_pointer_to_function_value(
339
339
const auto function_symbol = symbol_table.lookup (function_name);
340
340
if (function_symbol == nullptr )
341
341
{
342
- throw invalid_source_file_exceptiont {
342
+ throw invalid_input_exceptiont {
343
343
" input source code does not contain function: " + function_name};
344
344
}
345
345
CHECK_RETURN (function_symbol->type .id () == ID_code);
Original file line number Diff line number Diff line change @@ -95,6 +95,16 @@ std::string analysis_exceptiont::what() const
95
95
return reason;
96
96
}
97
97
98
+ invalid_input_exceptiont::invalid_input_exceptiont (std::string reason)
99
+ : m_reason(std::move(reason))
100
+ {
101
+ }
102
+
103
+ std::string invalid_input_exceptiont::what () const
104
+ {
105
+ return m_reason;
106
+ }
107
+
98
108
invalid_source_file_exceptiont::invalid_source_file_exceptiont (
99
109
std::string reason)
100
110
: reason(std::move(reason))
Original file line number Diff line number Diff line change @@ -164,6 +164,19 @@ class analysis_exceptiont : public cprover_exception_baset
164
164
std::string reason;
165
165
};
166
166
167
+ // / Thrown when user-provided input cannot be processed. Use
168
+ // / \ref invalid_source_file_exceptiont when the precise location of erroneous
169
+ // / input is known.
170
+ class invalid_input_exceptiont : public cprover_exception_baset
171
+ {
172
+ public:
173
+ explicit invalid_input_exceptiont (std::string reason);
174
+ std::string what () const override ;
175
+
176
+ protected:
177
+ std::string m_reason;
178
+ };
179
+
167
180
// / Thrown when we can't handle something in an input source file.
168
181
// / For example, if we get C source code that is not syntactically valid
169
182
// / or that has type errors.
Original file line number Diff line number Diff line change @@ -59,7 +59,7 @@ goto_modelt get_goto_model_from_c(std::istream &in)
59
59
const bool error = language.parse (in, " " );
60
60
61
61
if (error)
62
- throw invalid_source_file_exceptiont (" parsing failed" );
62
+ throw invalid_input_exceptiont (" parsing failed" );
63
63
}
64
64
65
65
language_file.get_modules ();
@@ -70,16 +70,15 @@ goto_modelt get_goto_model_from_c(std::istream &in)
70
70
const bool error = language_files.typecheck (goto_model.symbol_table );
71
71
72
72
if (error)
73
- throw invalid_source_file_exceptiont (" typechecking failed" );
73
+ throw invalid_input_exceptiont (" typechecking failed" );
74
74
}
75
75
76
76
{
77
77
const bool error =
78
78
language_files.generate_support_functions (goto_model.symbol_table );
79
79
80
80
if (error)
81
- throw invalid_source_file_exceptiont (
82
- " support function generation failed" );
81
+ throw invalid_input_exceptiont (" support function generation failed" );
83
82
}
84
83
85
84
goto_convert (
You can’t perform that action at this time.
0 commit comments