Skip to content

goto_cc_modet isn't a messaget #5618

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

Merged
kroening merged 1 commit into from
Dec 18, 2020
Merged

goto_cc_modet isn't a messaget #5618

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
5 changes: 3 additions & 2 deletions src/goto-cc/armcc_mode.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,10 +46,11 @@ int armcc_modet::doit()
has_prefix(base_name, "goto-link");
#endif

const auto verbosity = eval_verbosity(
const auto verbosity = messaget::eval_verbosity(
cmdline.get_value("verbosity"), messaget::M_ERROR, message_handler);

debug() << "ARM mode" << eom;
messaget log{message_handler};
log.debug() << "ARM mode" << messaget::eom;

// model validation
compiler.validate_goto_model = cmdline.isset("validate-goto-model");
Expand Down
50 changes: 30 additions & 20 deletions src/goto-cc/as_mode.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,8 @@ int as_modet::doit()
return EX_OK;
}

messaget log{message_handler};

bool act_as_as86=
base_name=="as86" ||
base_name.find("goto-as86")!=std::string::npos;
Expand All @@ -83,40 +85,44 @@ int as_modet::doit()
cmdline.isset("version"))
{
if(act_as_as86)
status() << "as86 version: 0.16.17 (goto-cc " << CBMC_VERSION << ")"
<< eom;
{
log.status() << "as86 version: 0.16.17 (goto-cc " << CBMC_VERSION << ")"
<< messaget::eom;
}
else
status() << "GNU assembler version 2.20.51.0.7 20100318"
<< " (goto-cc " << CBMC_VERSION << ")" << eom;
{
log.status() << "GNU assembler version 2.20.51.0.7 20100318"
<< " (goto-cc " << CBMC_VERSION << ")" << messaget::eom;
}

status()
log.status()
<< '\n'
<< "Copyright (C) 2006-2014 Daniel Kroening, Christoph Wintersteiger\n"
<< "CBMC version: " << CBMC_VERSION << '\n'
<< "Architecture: " << config.this_architecture() << '\n'
<< "OS: " << config.this_operating_system() << eom;
<< "OS: " << config.this_operating_system() << messaget::eom;

return EX_OK; // Exit!
}

auto default_verbosity = (cmdline.isset("w-") || cmdline.isset("warn")) ?
messaget::M_WARNING : messaget::M_ERROR;
eval_verbosity(
messaget::eval_verbosity(
cmdline.get_value("verbosity"), default_verbosity, message_handler);

if(act_as_as86)
{
if(produce_hybrid_binary)
debug() << "AS86 mode (hybrid)" << eom;
log.debug() << "AS86 mode (hybrid)" << messaget::eom;
else
debug() << "AS86 mode" << eom;
log.debug() << "AS86 mode" << messaget::eom;
}
else
{
if(produce_hybrid_binary)
debug() << "AS mode (hybrid)" << eom;
log.debug() << "AS mode (hybrid)" << messaget::eom;
else
debug() << "AS mode" << eom;
log.debug() << "AS mode" << messaget::eom;
}

// get configuration
Expand All @@ -128,12 +134,12 @@ int as_modet::doit()
if(cmdline.isset('b')) // as86 only
{
compiler.mode=compilet::COMPILE_LINK_EXECUTABLE;
debug() << "Compiling and linking an executable" << eom;
log.debug() << "Compiling and linking an executable" << messaget::eom;
}
else
{
compiler.mode=compilet::COMPILE_LINK;
debug() << "Compiling and linking a library" << eom;
log.debug() << "Compiling and linking a library" << messaget::eom;
}

config.ansi_c.mode=configt::ansi_ct::flavourt::GCC;
Expand Down Expand Up @@ -173,7 +179,7 @@ int as_modet::doit()
std::ifstream is(infile);
if(!is.is_open())
{
error() << "Failed to open input source " << infile << eom;
log.error() << "Failed to open input source " << infile << messaget::eom;
return 1;
}

Expand Down Expand Up @@ -208,7 +214,7 @@ int as_modet::doit()
os.open(dest);
if(!os.is_open())
{
error() << "Failed to tmp output file " << dest << eom;
log.error() << "Failed to tmp output file " << dest << messaget::eom;
return 1;
}

Expand All @@ -227,7 +233,10 @@ int as_modet::doit()
compiler.add_input_file(dest);
}
else
warning() << "No GOTO-CC section found in " << arg_it->arg << eom;
{
log.warning() << "No GOTO-CC section found in " << arg_it->arg
<< messaget::eom;
}
}

// Revert to as in case there is no source to compile
Expand Down Expand Up @@ -285,8 +294,9 @@ int as_modet::as_hybrid_binary(const compilet &compiler)
if(output_file=="/dev/null")
return EX_OK;

debug() << "Running " << native_tool_name
<< " to generate hybrid binary" << eom;
messaget log{message_handler};
log.debug() << "Running " << native_tool_name << " to generate hybrid binary"
<< messaget::eom;

// save the goto-cc output file
std::string saved = output_file + ".goto-cc-saved";
Expand All @@ -296,7 +306,7 @@ int as_modet::as_hybrid_binary(const compilet &compiler)
}
catch(const cprover_exception_baset &e)
{
error() << "Rename failed: " << e.what() << eom;
log.error() << "Rename failed: " << e.what() << messaget::eom;
return 1;
}

Expand All @@ -309,7 +319,7 @@ int as_modet::as_hybrid_binary(const compilet &compiler)
saved,
output_file,
compiler.mode == compilet::COMPILE_LINK_EXECUTABLE,
get_message_handler());
message_handler);
}

return result;
Expand Down
5 changes: 3 additions & 2 deletions src/goto-cc/cw_mode.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,10 +46,11 @@ int cw_modet::doit()
has_prefix(base_name, "goto-link");
#endif

const auto verbosity = eval_verbosity(
const auto verbosity = messaget::eval_verbosity(
cmdline.get_value("verbosity"), messaget::M_ERROR, message_handler);

debug() << "CodeWarrior mode" << eom;
messaget log{message_handler};
log.debug() << "CodeWarrior mode" << messaget::eom;

// model validation
compiler.validate_goto_model = cmdline.isset("validate-goto-model");
Expand Down
77 changes: 46 additions & 31 deletions src/goto-cc/gcc_mode.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -331,7 +331,7 @@ int gcc_modet::doit()

auto default_verbosity = (cmdline.isset("Wall") || cmdline.isset("Wextra")) ?
messaget::M_WARNING : messaget::M_ERROR;
eval_verbosity(
messaget::eval_verbosity(
cmdline.get_value("verbosity"), default_verbosity, gcc_message_handler);

bool act_as_bcc=
Expand Down Expand Up @@ -407,19 +407,21 @@ int gcc_modet::doit()
return EX_OK;
}

messaget log{gcc_message_handler};

if(act_as_bcc)
{
if(produce_hybrid_binary)
debug() << "BCC mode (hybrid)" << eom;
log.debug() << "BCC mode (hybrid)" << messaget::eom;
else
debug() << "BCC mode" << eom;
log.debug() << "BCC mode" << messaget::eom;
}
else
{
if(produce_hybrid_binary)
debug() << "GCC mode (hybrid)" << eom;
log.debug() << "GCC mode (hybrid)" << messaget::eom;
else
debug() << "GCC mode" << eom;
log.debug() << "GCC mode" << messaget::eom;
}

// model validation
Expand Down Expand Up @@ -540,25 +542,31 @@ int gcc_modet::doit()
switch(compiler.mode)
{
case compilet::LINK_LIBRARY:
debug() << "Linking a library only" << eom; break;
log.debug() << "Linking a library only" << messaget::eom;
break;
case compilet::COMPILE_ONLY:
debug() << "Compiling only" << eom; break;
log.debug() << "Compiling only" << messaget::eom;
break;
case compilet::ASSEMBLE_ONLY:
debug() << "Assembling only" << eom; break;
log.debug() << "Assembling only" << messaget::eom;
break;
case compilet::PREPROCESS_ONLY:
debug() << "Preprocessing only" << eom; break;
log.debug() << "Preprocessing only" << messaget::eom;
break;
case compilet::COMPILE_LINK:
debug() << "Compiling and linking a library" << eom; break;
log.debug() << "Compiling and linking a library" << messaget::eom;
break;
case compilet::COMPILE_LINK_EXECUTABLE:
debug() << "Compiling and linking an executable" << eom; break;
log.debug() << "Compiling and linking an executable" << messaget::eom;
break;
}

if(cmdline.isset("i386-win32") ||
cmdline.isset("winx64"))
{
// We may wish to reconsider the below.
config.ansi_c.mode=configt::ansi_ct::flavourt::VISUAL_STUDIO;
debug() << "Enabling Visual Studio syntax" << eom;
log.debug() << "Enabling Visual Studio syntax" << messaget::eom;
}
else
{
Expand Down Expand Up @@ -697,7 +705,7 @@ int gcc_modet::doit()

if(exit_code!=0)
{
error() << "preprocessing has failed" << eom;
log.error() << "preprocessing has failed" << messaget::eom;
return exit_code;
}

Expand Down Expand Up @@ -729,7 +737,8 @@ int gcc_modet::doit()
cmdline.isset('o') && cmdline.isset('c') &&
compiler.source_files.size() >= 2)
{
error() << "cannot specify -o with -c with multiple files" << eom;
log.error() << "cannot specify -o with -c with multiple files"
<< messaget::eom;
return 1; // to match gcc's behaviour
}

Expand Down Expand Up @@ -826,10 +835,11 @@ int gcc_modet::preprocess(
INVARIANT(new_argv.size()>=1, "No program name in argv");
new_argv[0]=native_tool_name.c_str();

debug() << "RUN:";
messaget log{gcc_message_handler};
log.debug() << "RUN:";
for(std::size_t i=0; i<new_argv.size(); i++)
debug() << " " << new_argv[i];
debug() << eom;
log.debug() << " " << new_argv[i];
log.debug() << messaget::eom;

return run(new_argv[0], new_argv, cmdline.stdin_file, stdout_file, "");
}
Expand Down Expand Up @@ -869,10 +879,11 @@ int gcc_modet::run_gcc(const compilet &compiler)
// overwrite argv[0]
new_argv[0]=native_tool_name;

debug() << "RUN:";
messaget log{gcc_message_handler};
log.debug() << "RUN:";
for(std::size_t i=0; i<new_argv.size(); i++)
debug() << " " << new_argv[i];
debug() << eom;
log.debug() << " " << new_argv[i];
log.debug() << messaget::eom;

return run(new_argv[0], new_argv, cmdline.stdin_file, "", "");
}
Expand Down Expand Up @@ -927,8 +938,9 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler)
output_files.front()=="/dev/null"))
return run_gcc(compiler);

debug() << "Running " << native_tool_name
<< " to generate hybrid binary" << eom;
messaget log{gcc_message_handler};
log.debug() << "Running " << native_tool_name << " to generate hybrid binary"
<< messaget::eom;

// save the goto-cc output files
std::list<std::string> goto_binaries;
Expand All @@ -945,7 +957,7 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler)
}
catch(const cprover_exception_baset &e)
{
error() << "Rename failed: " << e.what() << eom;
log.error() << "Rename failed: " << e.what() << messaget::eom;
return 1;
}

Expand Down Expand Up @@ -987,7 +999,7 @@ int gcc_modet::gcc_hybrid_binary(compilet &compiler)
goto_binary,
*it,
compiler.mode == compilet::COMPILE_LINK_EXECUTABLE,
get_message_handler());
gcc_message_handler);
}

return result;
Expand All @@ -1012,10 +1024,12 @@ int gcc_modet::asm_output(
return EX_OK;
}

messaget log{gcc_message_handler};

if(produce_hybrid_binary)
{
debug() << "Running " << native_tool_name
<< " to generate native asm output" << eom;
log.debug() << "Running " << native_tool_name
<< " to generate native asm output" << messaget::eom;

int result=run_gcc(compiler);
if(result!=0)
Expand Down Expand Up @@ -1043,23 +1057,24 @@ int gcc_modet::asm_output(
output_files.begin()->second=="/dev/null"))
return EX_OK;

debug()
<< "Appending preprocessed sources to generate hybrid asm output"
<< eom;
log.debug() << "Appending preprocessed sources to generate hybrid asm output"
<< messaget::eom;

for(const auto &so : output_files)
{
std::ifstream is(so.first);
if(!is.is_open())
{
error() << "Failed to open input source " << so.first << eom;
log.error() << "Failed to open input source " << so.first
<< messaget::eom;
return 1;
}

std::ofstream os(so.second, std::ios::app);
if(!os.is_open())
{
error() << "Failed to open output file " << so.second << eom;
log.error() << "Failed to open output file " << so.second
<< messaget::eom;
return 1;
}

Expand Down
Loading