Skip to content

Cleanup/initialise goto model #904

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 2 additions & 3 deletions src/goto-analyzer/goto_analyzer_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
#include <java_bytecode/java_bytecode_language.h>
#include <jsil/jsil_language.h>

#include <goto-programs/initialize_goto_model.h>
#include <goto-programs/set_properties.h>
#include <goto-programs/remove_function_pointers.h>
#include <goto-programs/remove_virtual_functions.h>
Expand Down Expand Up @@ -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))
Expand Down
4 changes: 2 additions & 2 deletions src/goto-analyzer/goto_analyzer_parse_options.h
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ Author: Daniel Kroening, [email protected]

#include <langapi/language_ui.h>

#include <goto-programs/get_goto_model.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/show_goto_functions.h>

#include <analyses/goto_check.h>
Expand Down Expand Up @@ -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();

Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -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 \
Expand Down
23 changes: 0 additions & 23 deletions src/goto-programs/get_goto_model.h

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -18,11 +18,11 @@ Author: Daniel Kroening, [email protected]

#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:

Expand All @@ -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<std::string> &files=_cmdline.args;
messaget msg(message_handler);
const std::vector<std::string> &files=cmdline.args;
if(files.empty())
{
error() << "Please provide a program" << eom;
msg.error() << "Please provide a program" << messaget::eom;
return true;
}

Expand All @@ -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)
{
Expand All @@ -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;
}

Expand All @@ -87,81 +91,78 @@ 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;
}
}
}

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;
}

Expand Down
22 changes: 22 additions & 0 deletions src/goto-programs/initialize_goto_model.h
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
/*******************************************************************\

Module: Initialize a Goto Program

Author: Daniel Kroening, [email protected]

\*******************************************************************/

#ifndef CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
#define CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H

#include <util/message.h>
#include <util/cmdline.h>

#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
5 changes: 2 additions & 3 deletions src/symex/symex_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
#include <cpp/cpp_language.h>
#include <java_bytecode/java_bytecode_language.h>

#include <goto-programs/initialize_goto_model.h>
#include <goto-programs/goto_convert_functions.h>
#include <goto-programs/show_properties.h>
#include <goto-programs/set_properties.h>
Expand Down Expand Up @@ -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))
Expand Down
4 changes: 2 additions & 2 deletions src/symex/symex_parse_options.h
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
#include <util/ui_message.h>
#include <util/parse_options.h>

#include <goto-programs/get_goto_model.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/show_goto_functions.h>

#include <langapi/language_ui.h>
Expand Down Expand Up @@ -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);
Expand Down