Skip to content

Commit 793fe3b

Browse files
Cleanup invariants in lazy_goto_model
1 parent 3ad3245 commit 793fe3b

File tree

1 file changed

+18
-14
lines changed

1 file changed

+18
-14
lines changed

src/goto-programs/lazy_goto_model.cpp

Lines changed: 18 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717
#include <langapi/language.h>
1818

1919
#include <fstream>
20+
#include <util/exception_utils.h>
2021

2122
//! @cond Doxygen_suppress_Lambda_in_initializer_list
2223
lazy_goto_modelt::lazy_goto_modelt(
@@ -94,8 +95,7 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
9495
const std::vector<std::string> &files=cmdline.args;
9596
if(files.empty())
9697
{
97-
msg.error() << "Please provide a program" << messaget::eom;
98-
throw 0;
98+
throw invalid_user_input_exceptiont("No program provided", "", "");
9999
}
100100

101101
std::vector<std::string> binaries, sources;
@@ -122,9 +122,8 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
122122

123123
if(!infile)
124124
{
125-
msg.error() << "failed to open input file `" << filename
126-
<< '\'' << messaget::eom;
127-
throw 0;
125+
throw system_exceptiont(
126+
"failed to open input file `" + filename + '\'');
128127
}
129128

130129
language_filet &lf=add_language_file(filename);
@@ -135,8 +134,10 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
135134
source_locationt location;
136135
location.set_file(filename);
137136
msg.error().source_location=location;
138-
msg.error() << "failed to figure out type of file" << messaget::eom;
139-
throw 0;
137+
throw deserialization_exceptiont(
138+
"failed to figure out type of file"
139+
"\nsource location: " +
140+
location.as_string());
140141
}
141142

142143
languaget &language=*lf.language;
@@ -147,8 +148,8 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
147148

148149
if(language.parse(infile, filename))
149150
{
150-
msg.error() << "PARSING ERROR" << messaget::eom;
151-
throw 0;
151+
// TODO more helpful error message
152+
throw deserialization_exceptiont("PARSING ERROR");
152153
}
153154

154155
lf.get_modules();
@@ -158,8 +159,8 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
158159

159160
if(language_files.typecheck(symbol_table))
160161
{
161-
msg.error() << "CONVERSION ERROR" << messaget::eom;
162-
throw 0;
162+
// TODO more helpful error message
163+
throw deserialization_exceptiont("CONVERSION ERROR");
163164
}
164165
}
165166

@@ -168,7 +169,10 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
168169
msg.status() << "Reading GOTO program from file" << messaget::eom;
169170

170171
if(read_object_and_link(file, *goto_model, message_handler))
171-
throw 0;
172+
{
173+
// TODO more helpful error message
174+
throw deserialization_exceptiont("Failed to read/link goto model");
175+
}
172176
}
173177

174178
bool binaries_provided_start =
@@ -203,8 +207,8 @@ void lazy_goto_modelt::initialize(const cmdlinet &cmdline)
203207

204208
if(entry_point_generation_failed)
205209
{
206-
msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
207-
throw 0;
210+
// TODO more helpful error message
211+
throw deserialization_exceptiont("SUPPORT FUNCTION GENERATION ERROR");
208212
}
209213

210214
// stupid hack

0 commit comments

Comments
 (0)