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;
@@ -689,15 +689,15 @@ bool cbmc_parse_optionst::set_properties()
 }
 
 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)
+ goto_modelt &goto_model,
+ const optionst &options,
+ const cmdlinet &cmdline,
+ 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

@@ -103,11 +103,10 @@ class cbmc_parse_optionst : public parse_options_baset, public xml_interfacet
   static bool process_goto_program(goto_modelt &, const optionst &, messaget &);
 
   static int get_goto_program(
-    goto_modelt &,
-    const optionst &,
-    const cmdlinet &,
-    messaget &,
-    ui_message_handlert &);
+   goto_modelt &,
+   const optionst &,
+   const cmdlinet &,
+   ui_message_handlert &);
 
 protected:
   goto_modelt goto_model;

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;