diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 5f889ff99d7..c783243a0d3 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -214,9 +215,7 @@ int goto_analyzer_parse_optionst::doit() register_languages(); - goto_model.set_message_handler(get_message_handler()); - - if(goto_model(cmdline)) + if(initialize_goto_model(goto_model, cmdline, get_message_handler())) return 6; if(process_goto_program(options)) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index a72dd9ca76a..538bf47ac3e 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include +#include #include #include @@ -56,7 +56,7 @@ class goto_analyzer_parse_optionst: protected: ui_message_handlert ui_message_handler; - get_goto_modelt goto_model; + goto_modelt goto_model; virtual void register_languages(); diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 94fc21b420c..fb3abf4ece3 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -6,7 +6,7 @@ SRC = basic_blocks.cpp \ destructor.cpp \ elf_reader.cpp \ format_strings.cpp \ - get_goto_model.cpp \ + initialize_goto_model.cpp \ goto_asm.cpp \ goto_clean_expr.cpp \ goto_convert.cpp \ diff --git a/src/goto-programs/get_goto_model.h b/src/goto-programs/get_goto_model.h deleted file mode 100644 index c2c8cfd1230..00000000000 --- a/src/goto-programs/get_goto_model.h +++ /dev/null @@ -1,23 +0,0 @@ -/*******************************************************************\ - -Module: Obtain a Goto Program - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#ifndef CPROVER_GOTO_PROGRAMS_GET_GOTO_MODEL_H -#define CPROVER_GOTO_PROGRAMS_GET_GOTO_MODEL_H - -#include -#include - -#include "goto_model.h" - -class get_goto_modelt:public goto_modelt, public messaget -{ -public: - bool operator()(const cmdlinet &); -}; - -#endif // CPROVER_GOTO_PROGRAMS_GET_GOTO_MODEL_H diff --git a/src/goto-programs/get_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp similarity index 59% rename from src/goto-programs/get_goto_model.cpp rename to src/goto-programs/initialize_goto_model.cpp index 9e594b37865..52a6caeeba2 100644 --- a/src/goto-programs/get_goto_model.cpp +++ b/src/goto-programs/initialize_goto_model.cpp @@ -18,11 +18,11 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_convert_functions.h" #include "read_goto_binary.h" -#include "get_goto_model.h" +#include "initialize_goto_model.h" /*******************************************************************\ -Function: get_goto_modelt::operator() +Function: initialize_goto_model Inputs: @@ -32,12 +32,16 @@ Function: get_goto_modelt::operator() \*******************************************************************/ -bool get_goto_modelt::operator()(const cmdlinet &_cmdline) +bool initialize_goto_model( + goto_modelt &goto_model, + const cmdlinet &cmdline, + message_handlert &message_handler) { - const std::vector &files=_cmdline.args; + messaget msg(message_handler); + const std::vector &files=cmdline.args; if(files.empty()) { - error() << "Please provide a program" << eom; + msg.error() << "Please provide a program" << messaget::eom; return true; } @@ -59,7 +63,7 @@ bool get_goto_modelt::operator()(const cmdlinet &_cmdline) { language_filest language_files; - language_files.set_message_handler(get_message_handler()); + language_files.set_message_handler(message_handler); for(const auto &filename : sources) { @@ -71,8 +75,8 @@ bool get_goto_modelt::operator()(const cmdlinet &_cmdline) if(!infile) { - error() << "failed to open input file `" << filename - << '\'' << eom; + msg.error() << "failed to open input file `" << filename + << '\'' << messaget::eom; return true; } @@ -87,38 +91,38 @@ bool get_goto_modelt::operator()(const cmdlinet &_cmdline) if(lf.language==NULL) { - error("failed to figure out type of file", filename); + msg.error("failed to figure out type of file", filename); return true; } languaget &language=*lf.language; - language.set_message_handler(get_message_handler()); - language.get_language_options(_cmdline); + language.set_message_handler(message_handler); + language.get_language_options(cmdline); - status() << "Parsing " << filename << eom; + msg.status() << "Parsing " << filename << messaget::eom; if(language.parse(infile, filename)) { - error() << "PARSING ERROR" << eom; + msg.error() << "PARSING ERROR" << messaget::eom; return true; } lf.get_modules(); } - status() << "Converting" << eom; + msg.status() << "Converting" << messaget::eom; - if(language_files.typecheck(symbol_table)) + if(language_files.typecheck(goto_model.symbol_table)) { - error() << "CONVERSION ERROR" << eom; + msg.error() << "CONVERSION ERROR" << messaget::eom; return true; } if(binaries.empty()) { - if(language_files.final(symbol_table)) + if(language_files.final(goto_model.symbol_table)) { - error() << "CONVERSION ERROR" << eom; + msg.error() << "CONVERSION ERROR" << messaget::eom; return true; } } @@ -126,42 +130,39 @@ bool get_goto_modelt::operator()(const cmdlinet &_cmdline) for(const auto &file : binaries) { - status() << "Reading GOTO program from file" << eom; + msg.status() << "Reading GOTO program from file" << messaget::eom; - if(read_object_and_link(file, *this, get_message_handler())) + if(read_object_and_link(file, goto_model, message_handler)) return true; } if(!binaries.empty()) - config.set_from_symbol_table(symbol_table); + config.set_from_symbol_table(goto_model.symbol_table); - status() << "Generating GOTO Program" << eom; + msg.status() << "Generating GOTO Program" << messaget::eom; - goto_convert(symbol_table, - goto_functions, - get_message_handler()); + goto_convert( + goto_model.symbol_table, + goto_model.goto_functions, + message_handler); } - catch(const char *e) { - error() << e << eom; + msg.error() << e << messaget::eom; return true; } - catch(const std::string e) { - error() << e << eom; + msg.error() << e << messaget::eom; return true; } - catch(int) { return true; } - catch(std::bad_alloc) { - error() << "Out of memory" << eom; + msg.error() << "Out of memory" << messaget::eom; return true; } diff --git a/src/goto-programs/initialize_goto_model.h b/src/goto-programs/initialize_goto_model.h new file mode 100644 index 00000000000..2b4b03615ca --- /dev/null +++ b/src/goto-programs/initialize_goto_model.h @@ -0,0 +1,22 @@ +/*******************************************************************\ + +Module: Initialize a Goto Program + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H +#define CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H + +#include +#include + +#include "goto_model.h" + +bool initialize_goto_model( + goto_modelt &goto_model, + const cmdlinet &cmdline, + message_handlert &message_handler); + +#endif // CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index 8001a5b8155..3b1b7f873a4 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -177,9 +178,7 @@ int symex_parse_optionst::doit() eval_verbosity(); - goto_model.set_message_handler(get_message_handler()); - - if(goto_model(cmdline)) + if(initialize_goto_model(goto_model, cmdline, get_message_handler())) return 6; if(process_goto_program(options)) diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h index 5e178eec14e..4a149e2147f 100644 --- a/src/symex/symex_parse_options.h +++ b/src/symex/symex_parse_options.h @@ -12,7 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include @@ -59,7 +59,7 @@ class symex_parse_optionst: protected: ui_message_handlert ui_message_handler; - get_goto_modelt goto_model; + goto_modelt goto_model; void get_command_line_options(optionst &options); bool process_goto_program(const optionst &options);