Skip to content

Commit ada2a90

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 a0fe71a commit ada2a90

File tree

6 files changed

+31
-10
lines changed

6 files changed

+31
-10
lines changed

jbmc/src/java_bytecode/java_bytecode_language.cpp

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

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

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

399398
// 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
@@ -152,14 +152,14 @@ void lazy_goto_modelt::initialize(
152152

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

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

160160
if(language_files.typecheck(symbol_table))
161161
{
162-
throw invalid_source_file_exceptiont("CONVERSION ERROR");
162+
throw invalid_input_exceptiont("CONVERSION ERROR");
163163
}
164164
}
165165
else

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
@@ -58,7 +58,7 @@ goto_modelt get_goto_model_from_c(std::istream &in)
5858
const bool error = language.parse(in, "");
5959

6060
if(error)
61-
throw invalid_source_file_exceptiont("parsing failed");
61+
throw invalid_input_exceptiont("parsing failed");
6262
}
6363

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

7171
if(error)
72-
throw invalid_source_file_exceptiont("typechecking failed");
72+
throw invalid_input_exceptiont("typechecking failed");
7373
}
7474

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

7979
if(error)
80-
throw invalid_source_file_exceptiont(
81-
"support function generation failed");
80+
throw invalid_input_exceptiont("support function generation failed");
8281
}
8382

8483
goto_convert(

0 commit comments

Comments
 (0)