Merge pull request #5618 from tautschnig/messaget-goto_cc_mode

goto_cc_modet isn't a messaget

Author: kroening

src/goto-cc/armcc_mode.cpp

@@ -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");

src/goto-cc/as_mode.cpp

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

src/goto-cc/cw_mode.cpp

@@ -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");

src/goto-cc/gcc_mode.cpp

@@ -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=
@@ -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
@@ -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
   {
@@ -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;
           }
 
@@ -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
   }
 
@@ -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, "");
 }
@@ -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, "", "");
 }
@@ -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;
@@ -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;
     }
 
@@ -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;
@@ -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)
@@ -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;
     }