Remove unecessary log argument in cbmc_parse_optionst

The messaget can be constructed from the message_handler.

Author: romainbrenguier

src/cbmc/cbmc_parse_options.cpp

@@ -547,7 +547,7 @@ int cbmc_parse_optionst::doit()
   }
 
   int get_goto_program_ret =
-    get_goto_program(goto_model, options, cmdline, log, ui_message_handler);
+    get_goto_program(goto_model, options, cmdline, ui_message_handler);
 
   if(get_goto_program_ret!=-1)
     return get_goto_program_ret;
@@ -692,12 +692,12 @@ int cbmc_parse_optionst::get_goto_program(
   goto_modelt &goto_model,
   const optionst &options,
   const cmdlinet &cmdline,
-  messaget &log,
   ui_message_handlert &ui_message_handler)
 {
+  messaget log{ui_message_handler};
   if(cmdline.args.empty())
   {
-    log.error() << "Please provide a program to verify" << log.eom;
+    log.error() << "Please provide a program to verify" << messaget::eom;
     return CPROVER_EXIT_INCORRECT_TASK;
   }
 
@@ -739,7 +739,7 @@ int cbmc_parse_optionst::get_goto_program(
       return CPROVER_EXIT_SUCCESS;
     }
 
-    log.status() << config.object_bits_info() << log.eom;
+    log.status() << config.object_bits_info() << messaget::eom;
   }
 
   return -1; // no error, continue

src/cbmc/cbmc_parse_options.h

@@ -106,7 +106,6 @@ class cbmc_parse_optionst : public parse_options_baset, public xml_interfacet
     goto_modelt &,
     const optionst &,
     const cmdlinet &,
-    messaget &,
     ui_message_handlert &);
 
 protected:

unit/compound_block_locations.cpp

@@ -289,7 +289,7 @@ void compound_block_locationst::check_compound_block_locations(
 
   goto_modelt gm;
   int ret;
-  ret = cbmc_parse_optionst::get_goto_program(gm, opts, cmdline, log, mh);
+  ret = cbmc_parse_optionst::get_goto_program(gm, opts, cmdline, mh);
   REQUIRE(ret == -1);
 
   const auto found = gm.goto_functions.function_map.find("main");

unit/path_strategies.cpp

@@ -398,7 +398,7 @@ void _check_with_strategy(
   goto_modelt goto_model;
   int ret;
   ret = cbmc_parse_optionst::get_goto_program(
-    goto_model, options, cmdline, log, ui_message_handler);
+    goto_model, options, cmdline, ui_message_handler);
   REQUIRE(ret == -1);
 
   symbol_tablet symex_symbol_table;