Skip to content
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.

Sign up for GitHub

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

goto_analyzer_parse_optionst is not a messaget #4517

Merged
merged 1 commit into from
Apr 11, 2019
Merged

goto_analyzer_parse_optionst is not a messaget #4517

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
85 changes: 40 additions & 45 deletions src/goto-analyzer/goto_analyzer_parse_options.cpp
View file
Open in desktop
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
Open in desktop
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