Skip to content

Commit

Permalink
Merge pull request diffblue#4517 from romainbrenguier/clean-up/goto-a…
Browse files Browse the repository at this point in the history 
…nalyzer-messaget

goto_analyzer_parse_optionst is not a messaget
  • Loading branch information
@romainbrenguier
romainbrenguier authored Apr 11, 2019
2 parents 0ae5255 + 27baa38 commit eed359b
Show file tree
Hide file tree
Showing 2 changed files with 41 additions and 48 deletions.
85 changes: 40 additions & 45 deletions src/goto-analyzer/goto_analyzer_parse_options.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,6 @@ goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
int argc,
const char **argv)
: parse_options_baset(GOTO_ANALYSER_OPTIONS, argc, argv, ui_message_handler),
messaget(ui_message_handler),
ui_message_handler(cmdline, std::string("GOTO-ANALYZER ") + CBMC_VERSION)
{
}
Expand Down Expand Up @@ -298,7 +297,8 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
if(!options.get_bool_option("domain set"))
{
// Default to constants as it is light-weight but useful
status() << "Domain not specified, defaulting to --constants" << eom;
log.status() << "Domain not specified, defaulting to --constants"
<< messaget::eom;
options.set_option("constants", true);
}
}
Expand Down Expand Up @@ -386,20 +386,20 @@ int goto_analyzer_parse_optionst::doit()

optionst options;
get_command_line_options(options);
eval_verbosity(
messaget::eval_verbosity(
cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);

//
// Print a banner
//
status() << "GOTO-ANALYSER version " << CBMC_VERSION << " "
<< sizeof(void *) * 8 << "-bit " << config.this_architecture() << " "
<< config.this_operating_system() << eom;
log.status() << "GOTO-ANALYSER version " << CBMC_VERSION << " "
<< sizeof(void *) * 8 << "-bit " << config.this_architecture()
<< " " << config.this_operating_system() << messaget::eom;

register_languages();

goto_model =
initialize_goto_model(cmdline.args, get_message_handler(), options);
initialize_goto_model(cmdline.args, log.get_message_handler(), options);

if(process_goto_program(options))
return CPROVER_EXIT_INTERNAL_ERROR;
Expand All @@ -423,7 +423,7 @@ int goto_analyzer_parse_optionst::doit()
{
show_goto_functions(
goto_model,
get_message_handler(),
log.get_message_handler(),
get_ui(),
cmdline.isset("list-goto-functions"));
return CPROVER_EXIT_SUCCESS;
Expand All @@ -443,15 +443,15 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)

if(cmdline.isset("show-taint"))
{
taint_analysis(goto_model, taint_file, get_message_handler(), true, "");
taint_analysis(
goto_model, taint_file, log.get_message_handler(), true, "");
return CPROVER_EXIT_SUCCESS;
}
else
{
std::string json_file=cmdline.get_value("json");
bool result=
taint_analysis(
goto_model, taint_file, get_message_handler(), false, json_file);
bool result = taint_analysis(
goto_model, taint_file, log.get_message_handler(), false, json_file);
return result ? CPROVER_EXIT_VERIFICATION_UNSAFE : CPROVER_EXIT_SUCCESS;
}
}
Expand All @@ -471,8 +471,8 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
std::ofstream ofs(json_file);
if(!ofs)
{
error() << "Failed to open json output `"
<< json_file << "'" << eom;
log.error() << "Failed to open json output `" << json_file << "'"
<< messaget::eom;
return CPROVER_EXIT_INTERNAL_ERROR;
}

Expand All @@ -496,8 +496,8 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
std::ofstream ofs(json_file);
if(!ofs)
{
error() << "Failed to open json output `"
<< json_file << "'" << eom;
log.error() << "Failed to open json output `" << json_file << "'"
<< messaget::eom;
return CPROVER_EXIT_INTERNAL_ERROR;
}

Expand All @@ -521,8 +521,8 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
std::ofstream ofs(json_file);
if(!ofs)
{
error() << "Failed to open json output `"
<< json_file << "'" << eom;
log.error() << "Failed to open json output `" << json_file << "'"
<< messaget::eom;
return CPROVER_EXIT_INTERNAL_ERROR;
}

Expand Down Expand Up @@ -553,7 +553,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)

if(cmdline.isset("show-properties"))
{
show_properties(goto_model, get_message_handler(), get_ui());
show_properties(goto_model, log.get_message_handler(), get_ui());
return CPROVER_EXIT_SUCCESS;
}

Expand All @@ -574,29 +574,29 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)

if(!out)
{
error() << "Failed to open output file `"
<< outfile << "'" << eom;
log.error() << "Failed to open output file `" << outfile << "'"
<< messaget::eom;
return CPROVER_EXIT_INTERNAL_ERROR;
}

// Build analyzer
status() << "Selecting abstract domain" << eom;
log.status() << "Selecting abstract domain" << messaget::eom;
namespacet ns(goto_model.symbol_table); // Must live as long as the domain.
std::unique_ptr<ai_baset> analyzer(build_analyzer(options, ns));

if(analyzer == nullptr)
{
status() << "Task / Interpreter / Domain combination not supported"
<< messaget::eom;
log.status() << "Task / Interpreter / Domain combination not supported"
<< messaget::eom;
return CPROVER_EXIT_INTERNAL_ERROR;
}

// Run
status() << "Computing abstract states" << eom;
log.status() << "Computing abstract states" << messaget::eom;
(*analyzer)(goto_model);

// Perform the task
status() << "Performing task" << eom;
log.status() << "Performing task" << messaget::eom;

bool result = true;

Expand All @@ -607,27 +607,21 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
}
else if(options.get_bool_option("show-on-source"))
{
show_on_source(goto_model, *analyzer, get_message_handler());
show_on_source(goto_model, *analyzer, log.get_message_handler());
return CPROVER_EXIT_SUCCESS;
}
else if(options.get_bool_option("verify"))
{
result = static_verifier(goto_model,
*analyzer,
options,
get_message_handler(),
out);
result = static_verifier(
goto_model, *analyzer, options, log.get_message_handler(), out);
}
else if(options.get_bool_option("simplify"))
{
PRECONDITION(!outfile.empty() && outfile != "-");
output_stream.close();
output_stream.open(outfile, std::ios::binary);
result = static_simplifier(goto_model,
*analyzer,
options,
get_message_handler(),
out);
result = static_simplifier(
goto_model, *analyzer, options, log.get_message_handler(), out);
}
else if(options.get_bool_option("unreachable-instructions"))
{
Expand All @@ -652,7 +646,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
}
else
{
error() << "Unhandled task" << eom;
log.error() << "Unhandled task" << messaget::eom;
return CPROVER_EXIT_INTERNAL_ERROR;
}

Expand All @@ -662,8 +656,8 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)


// Final defensive error case
error() << "no analysis option given -- consider reading --help"
<< eom;
log.error() << "no analysis option given -- consider reading --help"
<< messaget::eom;
return CPROVER_EXIT_USAGE_ERROR;
}

Expand All @@ -677,19 +671,20 @@ bool goto_analyzer_parse_optionst::process_goto_program(
remove_asm(goto_model);

// add the library
status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << messaget::eom;
link_to_library(
goto_model, ui_message_handler, cprover_cpp_library_factory);
link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
#endif

// remove function pointers
status() << "Removing function pointers and virtual functions" << eom;
log.status() << "Removing function pointers and virtual functions"
<< messaget::eom;
remove_function_pointers(
get_message_handler(), goto_model, cmdline.isset("pointer-check"));
log.get_message_handler(), goto_model, cmdline.isset("pointer-check"));

// do partial inlining
status() << "Partial Inlining" << eom;
log.status() << "Partial Inlining" << messaget::eom;
goto_partial_inline(goto_model, ui_message_handler);

// remove returns, gcc vectors, complex
Expand All @@ -699,7 +694,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(

#if 0
// add generic checks
status() << "Generic Property Instrumentation" << eom;
log.status() << "Generic Property Instrumentation" << messaget::eom;
goto_check(options, goto_model);
#else
(void)options; // unused parameter
Expand Down
4 changes: 1 addition & 3 deletions src/goto-analyzer/goto_analyzer_parse_options.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -153,9 +153,7 @@ class optionst;
OPT_VALIDATE \
// clang-format on

class goto_analyzer_parse_optionst:
public parse_options_baset,
public messaget
class goto_analyzer_parse_optionst: public parse_options_baset
{
public:
virtual int doit() override;
Expand Down

0 comments on commit eed359b

Please sign in to comment.