Skip to content

Commit 6c6304f

Browse files
committed
Do not use invalid_source_file_exceptiont without source location
In preparation of tying invalid_source_file_exceptiont to an actual source location, introduce an exception that is thrown when some invalid input is encountered, but a precise source location is not known at the time of throwing the exception.
1 parent abba3d7 commit 6c6304f

File tree

7 files changed

+33
-12
lines changed

7 files changed

+33
-12
lines changed

jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -319,7 +319,7 @@ void java_bytecode_languaget::initialize_class_loader()
319319

320320
static void throwMainClassLoadingError(const std::string &main_class)
321321
{
322-
throw invalid_source_file_exceptiont(
322+
throw system_exceptiont(
323323
"Error: Could not find or load main class " + main_class);
324324
}
325325

@@ -393,8 +393,7 @@ bool java_bytecode_languaget::parse(
393393
std::ifstream jar_file(path);
394394
if(!jar_file.good())
395395
{
396-
throw invalid_source_file_exceptiont(
397-
"Error: Unable to access jarfile " + path);
396+
throw system_exceptiont("Error: Unable to access jarfile " + path);
398397
}
399398

400399
// build an object to potentially limit which classes are loaded

jbmc/src/java_bytecode/lazy_goto_model.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -151,14 +151,14 @@ void lazy_goto_modelt::initialize(
151151

152152
if(dynamic_cast<java_bytecode_languaget &>(language).parse())
153153
{
154-
throw invalid_source_file_exceptiont("PARSING ERROR");
154+
throw invalid_input_exceptiont("PARSING ERROR");
155155
}
156156

157157
msg.status() << "Converting" << messaget::eom;
158158

159159
if(language_files.typecheck(symbol_table))
160160
{
161-
throw invalid_source_file_exceptiont("CONVERSION ERROR");
161+
throw invalid_input_exceptiont("CONVERSION ERROR");
162162
}
163163
}
164164
else

src/goto-programs/link_goto_model.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -181,7 +181,7 @@ void link_goto_model(
181181

182182
if(linking.typecheck_main())
183183
{
184-
throw invalid_source_file_exceptiont("typechecking main failed");
184+
throw invalid_input_exceptiont("typechecking main failed");
185185
}
186186
if(link_functions(
187187
dest.symbol_table,
@@ -192,6 +192,6 @@ void link_goto_model(
192192
weak_symbols,
193193
linking.object_type_updates))
194194
{
195-
throw invalid_source_file_exceptiont("linking failed");
195+
throw invalid_input_exceptiont("linking failed");
196196
}
197197
}

src/memory-analyzer/analyze_symbol.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -339,7 +339,7 @@ exprt gdb_value_extractort::get_pointer_to_function_value(
339339
const auto function_symbol = symbol_table.lookup(function_name);
340340
if(function_symbol == nullptr)
341341
{
342-
throw invalid_source_file_exceptiont{
342+
throw invalid_input_exceptiont{
343343
"input source code does not contain function: " + function_name};
344344
}
345345
CHECK_RETURN(function_symbol->type.id() == ID_code);

src/util/exception_utils.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,16 @@ std::string analysis_exceptiont::what() const
9595
return reason;
9696
}
9797

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+
98108
invalid_source_file_exceptiont::invalid_source_file_exceptiont(
99109
std::string reason)
100110
: reason(std::move(reason))

src/util/exception_utils.h

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -164,6 +164,19 @@ class analysis_exceptiont : public cprover_exception_baset
164164
std::string reason;
165165
};
166166

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+
167180
/// Thrown when we can't handle something in an input source file.
168181
/// For example, if we get C source code that is not syntactically valid
169182
/// or that has type errors.

unit/testing-utils/get_goto_model_from_c.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ goto_modelt get_goto_model_from_c(std::istream &in)
5959
const bool error = language.parse(in, "");
6060

6161
if(error)
62-
throw invalid_source_file_exceptiont("parsing failed");
62+
throw invalid_input_exceptiont("parsing failed");
6363
}
6464

6565
language_file.get_modules();
@@ -70,16 +70,15 @@ goto_modelt get_goto_model_from_c(std::istream &in)
7070
const bool error = language_files.typecheck(goto_model.symbol_table);
7171

7272
if(error)
73-
throw invalid_source_file_exceptiont("typechecking failed");
73+
throw invalid_input_exceptiont("typechecking failed");
7474
}
7575

7676
{
7777
const bool error =
7878
language_files.generate_support_functions(goto_model.symbol_table);
7979

8080
if(error)
81-
throw invalid_source_file_exceptiont(
82-
"support function generation failed");
81+
throw invalid_input_exceptiont("support function generation failed");
8382
}
8483

8584
goto_convert(

0 commit comments

Comments
 (0)