Skip to content

Commit bd37426

Browse files
author
Daniel Kroening
authored
Merge pull request #904 from NathanJPhillips/cleanup/initialise-goto-model
Cleanup/initialise goto model
2 parents fc4c0fe + cfad717 commit bd37426

8 files changed

+64
-66
lines changed

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
1616
#include <java_bytecode/java_bytecode_language.h>
1717
#include <jsil/jsil_language.h>
1818

19+
#include <goto-programs/initialize_goto_model.h>
1920
#include <goto-programs/set_properties.h>
2021
#include <goto-programs/remove_function_pointers.h>
2122
#include <goto-programs/remove_virtual_functions.h>
@@ -214,9 +215,7 @@ int goto_analyzer_parse_optionst::doit()
214215

215216
register_languages();
216217

217-
goto_model.set_message_handler(get_message_handler());
218-
219-
if(goto_model(cmdline))
218+
if(initialize_goto_model(goto_model, cmdline, get_message_handler()))
220219
return 6;
221220

222221
if(process_goto_program(options))

‎src/goto-analyzer/goto_analyzer_parse_options.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]
1414

1515
#include <langapi/language_ui.h>
1616

17-
#include <goto-programs/get_goto_model.h>
17+
#include <goto-programs/goto_model.h>
1818
#include <goto-programs/show_goto_functions.h>
1919

2020
#include <analyses/goto_check.h>
@@ -56,7 +56,7 @@ class goto_analyzer_parse_optionst:
5656

5757
protected:
5858
ui_message_handlert ui_message_handler;
59-
get_goto_modelt goto_model;
59+
goto_modelt goto_model;
6060

6161
virtual void register_languages();
6262

‎src/goto-programs/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ SRC = basic_blocks.cpp \
66
destructor.cpp \
77
elf_reader.cpp \
88
format_strings.cpp \
9-
get_goto_model.cpp \
9+
initialize_goto_model.cpp \
1010
goto_asm.cpp \
1111
goto_clean_expr.cpp \
1212
goto_convert.cpp \

‎src/goto-programs/get_goto_model.h

-23
This file was deleted.

‎src/goto-programs/get_goto_model.cpp renamed to ‎src/goto-programs/initialize_goto_model.cpp

+33-32
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,11 @@ Author: Daniel Kroening, [email protected]
1818

1919
#include "goto_convert_functions.h"
2020
#include "read_goto_binary.h"
21-
#include "get_goto_model.h"
21+
#include "initialize_goto_model.h"
2222

2323
/*******************************************************************\
2424
25-
Function: get_goto_modelt::operator()
25+
Function: initialize_goto_model
2626
2727
Inputs:
2828
@@ -32,12 +32,16 @@ Function: get_goto_modelt::operator()
3232
3333
\*******************************************************************/
3434

35-
bool get_goto_modelt::operator()(const cmdlinet &_cmdline)
35+
bool initialize_goto_model(
36+
goto_modelt &goto_model,
37+
const cmdlinet &cmdline,
38+
message_handlert &message_handler)
3639
{
37-
const std::vector<std::string> &files=_cmdline.args;
40+
messaget msg(message_handler);
41+
const std::vector<std::string> &files=cmdline.args;
3842
if(files.empty())
3943
{
40-
error() << "Please provide a program" << eom;
44+
msg.error() << "Please provide a program" << messaget::eom;
4145
return true;
4246
}
4347

@@ -59,7 +63,7 @@ bool get_goto_modelt::operator()(const cmdlinet &_cmdline)
5963
{
6064
language_filest language_files;
6165

62-
language_files.set_message_handler(get_message_handler());
66+
language_files.set_message_handler(message_handler);
6367

6468
for(const auto &filename : sources)
6569
{
@@ -71,8 +75,8 @@ bool get_goto_modelt::operator()(const cmdlinet &_cmdline)
7175

7276
if(!infile)
7377
{
74-
error() << "failed to open input file `" << filename
75-
<< '\'' << eom;
78+
msg.error() << "failed to open input file `" << filename
79+
<< '\'' << messaget::eom;
7680
return true;
7781
}
7882

@@ -87,81 +91,78 @@ bool get_goto_modelt::operator()(const cmdlinet &_cmdline)
8791

8892
if(lf.language==NULL)
8993
{
90-
error("failed to figure out type of file", filename);
94+
msg.error("failed to figure out type of file", filename);
9195
return true;
9296
}
9397

9498
languaget &language=*lf.language;
95-
language.set_message_handler(get_message_handler());
96-
language.get_language_options(_cmdline);
99+
language.set_message_handler(message_handler);
100+
language.get_language_options(cmdline);
97101

98-
status() << "Parsing " << filename << eom;
102+
msg.status() << "Parsing " << filename << messaget::eom;
99103

100104
if(language.parse(infile, filename))
101105
{
102-
error() << "PARSING ERROR" << eom;
106+
msg.error() << "PARSING ERROR" << messaget::eom;
103107
return true;
104108
}
105109

106110
lf.get_modules();
107111
}
108112

109-
status() << "Converting" << eom;
113+
msg.status() << "Converting" << messaget::eom;
110114

111-
if(language_files.typecheck(symbol_table))
115+
if(language_files.typecheck(goto_model.symbol_table))
112116
{
113-
error() << "CONVERSION ERROR" << eom;
117+
msg.error() << "CONVERSION ERROR" << messaget::eom;
114118
return true;
115119
}
116120

117121
if(binaries.empty())
118122
{
119-
if(language_files.final(symbol_table))
123+
if(language_files.final(goto_model.symbol_table))
120124
{
121-
error() << "CONVERSION ERROR" << eom;
125+
msg.error() << "CONVERSION ERROR" << messaget::eom;
122126
return true;
123127
}
124128
}
125129
}
126130

127131
for(const auto &file : binaries)
128132
{
129-
status() << "Reading GOTO program from file" << eom;
133+
msg.status() << "Reading GOTO program from file" << messaget::eom;
130134

131-
if(read_object_and_link(file, *this, get_message_handler()))
135+
if(read_object_and_link(file, goto_model, message_handler))
132136
return true;
133137
}
134138

135139
if(!binaries.empty())
136-
config.set_from_symbol_table(symbol_table);
140+
config.set_from_symbol_table(goto_model.symbol_table);
137141

138-
status() << "Generating GOTO Program" << eom;
142+
msg.status() << "Generating GOTO Program" << messaget::eom;
139143

140-
goto_convert(symbol_table,
141-
goto_functions,
142-
get_message_handler());
144+
goto_convert(
145+
goto_model.symbol_table,
146+
goto_model.goto_functions,
147+
message_handler);
143148
}
144-
145149
catch(const char *e)
146150
{
147-
error() << e << eom;
151+
msg.error() << e << messaget::eom;
148152
return true;
149153
}
150-
151154
catch(const std::string e)
152155
{
153-
error() << e << eom;
156+
msg.error() << e << messaget::eom;
154157
return true;
155158
}
156-
157159
catch(int)
158160
{
159161
return true;
160162
}
161-
162163
catch(std::bad_alloc)
163164
{
164-
error() << "Out of memory" << eom;
165+
msg.error() << "Out of memory" << messaget::eom;
165166
return true;
166167
}
167168

‎src/goto-programs/initialize_goto_model.h

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
/*******************************************************************\
2+
3+
Module: Initialize a Goto Program
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
10+
#define CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
11+
12+
#include <util/message.h>
13+
#include <util/cmdline.h>
14+
15+
#include "goto_model.h"
16+
17+
bool initialize_goto_model(
18+
goto_modelt &goto_model,
19+
const cmdlinet &cmdline,
20+
message_handlert &message_handler);
21+
22+
#endif // CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H

‎src/symex/symex_parse_options.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
2121
#include <cpp/cpp_language.h>
2222
#include <java_bytecode/java_bytecode_language.h>
2323

24+
#include <goto-programs/initialize_goto_model.h>
2425
#include <goto-programs/goto_convert_functions.h>
2526
#include <goto-programs/show_properties.h>
2627
#include <goto-programs/set_properties.h>
@@ -177,9 +178,7 @@ int symex_parse_optionst::doit()
177178

178179
eval_verbosity();
179180

180-
goto_model.set_message_handler(get_message_handler());
181-
182-
if(goto_model(cmdline))
181+
if(initialize_goto_model(goto_model, cmdline, get_message_handler()))
183182
return 6;
184183

185184
if(process_goto_program(options))

‎src/symex/symex_parse_options.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#include <util/ui_message.h>
1313
#include <util/parse_options.h>
1414

15-
#include <goto-programs/get_goto_model.h>
15+
#include <goto-programs/goto_model.h>
1616
#include <goto-programs/show_goto_functions.h>
1717

1818
#include <langapi/language_ui.h>
@@ -59,7 +59,7 @@ class symex_parse_optionst:
5959

6060
protected:
6161
ui_message_handlert ui_message_handler;
62-
get_goto_modelt goto_model;
62+
goto_modelt goto_model;
6363

6464
void get_command_line_options(optionst &options);
6565
bool process_goto_program(const optionst &options);

0 commit comments

Comments
 (0)