Skip to content

Commit 5ed1623

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 c351198 commit 5ed1623

File tree

9 files changed

+37
-16
lines changed

9 files changed

+37
-16
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/crangler/ctokenit.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ ctokenitt match_bracket(ctokenitt t, char open, char close)
4646
while(true)
4747
{
4848
if(!t)
49-
throw invalid_source_file_exceptiont("expected " + std::string(1, close));
49+
throw invalid_input_exceptiont("expected " + std::string(1, close));
5050

5151
const auto &token = *(t++);
5252

src/crangler/mini_c_parser.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -143,7 +143,7 @@ void mini_c_parsert::parse_brackets(char open, char close, tokenst &dest)
143143
while(true)
144144
{
145145
if(eof())
146-
throw invalid_source_file_exceptiont("expected " + std::string(1, close));
146+
throw invalid_input_exceptiont("expected " + std::string(1, close));
147147

148148
auto &token = consume_token();
149149
dest.push_back(token);
@@ -297,7 +297,7 @@ mini_c_parsert::tokenst mini_c_parsert::parse_initializer()
297297
while(true)
298298
{
299299
if(eof())
300-
throw invalid_source_file_exceptiont("expected an initializer");
300+
throw invalid_input_exceptiont("expected an initializer");
301301
auto &token = consume_token();
302302
result.push_back(token);
303303
if(token == ';')
@@ -317,7 +317,7 @@ mini_c_parsert::tokenst mini_c_parsert::parse_initializer()
317317
while(true)
318318
{
319319
if(eof())
320-
throw invalid_source_file_exceptiont("eof in function body");
320+
throw invalid_input_exceptiont("eof in function body");
321321
auto &token = consume_token();
322322
result.push_back(token);
323323
if(token == '{')

src/memory-analyzer/analyze_symbol.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -350,7 +350,7 @@ exprt gdb_value_extractort::get_pointer_to_function_value(
350350
const auto function_symbol = symbol_table.lookup(function_name);
351351
if(function_symbol == nullptr)
352352
{
353-
throw invalid_source_file_exceptiont{
353+
throw invalid_input_exceptiont{
354354
"input source code does not contain function: " + function_name};
355355
}
356356
CHECK_RETURN(function_symbol->type.id() == ID_code);

src/symtab2gb/symtab2gb_parse_options.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -90,8 +90,8 @@ static void run_symtab2gb(
9090

9191
if(failed(linking(linked_symbol_table, symtab, message_handler)))
9292
{
93-
throw invalid_source_file_exceptiont{"failed to link `" +
94-
symtab_filename + "'"};
93+
throw invalid_input_exceptiont{
94+
"failed to link `" + symtab_filename + "'"};
9595
}
9696
}
9797

src/util/exception_utils.cpp

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,16 @@ analysis_exceptiont::analysis_exceptiont(std::string reason)
8080
{
8181
}
8282

83+
invalid_input_exceptiont::invalid_input_exceptiont(std::string reason)
84+
: m_reason(std::move(reason))
85+
{
86+
}
87+
88+
std::string invalid_input_exceptiont::what() const
89+
{
90+
return m_reason;
91+
}
92+
8393
invalid_source_file_exceptiont::invalid_source_file_exceptiont(
8494
std::string reason)
8595
: cprover_exception_baset(std::move(reason))

src/util/exception_utils.h

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -156,6 +156,19 @@ class analysis_exceptiont : public cprover_exception_baset
156156
explicit analysis_exceptiont(std::string reason);
157157
};
158158

159+
/// Thrown when user-provided input cannot be processed. Use
160+
/// \ref invalid_source_file_exceptiont when the precise location of erroneous
161+
/// input is known.
162+
class invalid_input_exceptiont : public cprover_exception_baset
163+
{
164+
public:
165+
explicit invalid_input_exceptiont(std::string reason);
166+
std::string what() const override;
167+
168+
protected:
169+
std::string m_reason;
170+
};
171+
159172
/// Thrown when we can't handle something in an input source file.
160173
/// For example, if we get C source code that is not syntactically valid
161174
/// 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)