Show properties take a ui_message_handlert

This is more precise on the type of message handler we are expecting and
makes the ui argument redundant.

Author: romainbrenguier

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -520,8 +520,7 @@ int janalyzer_parse_optionst::perform_analysis(const optionst &options)
 
   if(cmdline.isset("show-properties"))
   {
-    show_properties(
-      goto_model, ui_message_handler, ui_message_handler.get_ui());
+    show_properties(goto_model, ui_message_handler);
     return CPROVER_EXIT_SUCCESS;
   }
 

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -563,8 +563,7 @@ int jbmc_parse_optionst::doit()
 
     if(cmdline.isset("show-properties"))
     {
-      show_properties(
-        goto_model, ui_message_handler, ui_message_handler.get_ui());
+      show_properties(goto_model, ui_message_handler);
       return 0; // should contemplate EX_OK from sysexits.h
     }
 
@@ -940,11 +939,7 @@ bool jbmc_parse_optionst::show_loaded_functions(
   if(cmdline.isset("show-properties"))
   {
     namespacet ns(goto_model.get_symbol_table());
-    show_properties(
-      ns,
-      ui_message_handler,
-      ui_message_handler.get_ui(),
-      goto_model.get_goto_functions());
+    show_properties(ns, ui_message_handler, goto_model.get_goto_functions());
     return true;
   }
 

src/cbmc/cbmc_parse_options.cpp

@@ -555,8 +555,7 @@ int cbmc_parse_optionst::doit()
   if(cmdline.isset("show-claims") || // will go away
      cmdline.isset("show-properties")) // use this one
   {
-    show_properties(
-      goto_model, ui_message_handler, ui_message_handler.get_ui());
+    show_properties(goto_model, ui_message_handler);
     return CPROVER_EXIT_SUCCESS;
   }
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -554,8 +554,7 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
   if(cmdline.isset("show-properties"))
   {
-    show_properties(
-      goto_model, ui_message_handler, ui_message_handler.get_ui());
+    show_properties(goto_model, ui_message_handler);
     return CPROVER_EXIT_SUCCESS;
   }
 

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -565,8 +565,7 @@ int goto_instrument_parse_optionst::doit()
        cmdline.isset("show-properties"))
     {
       const namespacet ns(goto_model.symbol_table);
-      show_properties(
-        goto_model, ui_message_handler, ui_message_handler.get_ui());
+      show_properties(goto_model, ui_message_handler);
       return CPROVER_EXIT_SUCCESS;
     }
 

src/goto-programs/show_properties.cpp

@@ -163,25 +163,25 @@ void show_properties_json(
 
 void show_properties(
   const namespacet &ns,
-  message_handlert &message_handler,
-  ui_message_handlert::uit ui,
+  ui_message_handlert &ui_message_handler,
   const goto_functionst &goto_functions)
 {
+  ui_message_handlert::uit ui = ui_message_handler.get_ui();
   if(ui == ui_message_handlert::uit::JSON_UI)
-    show_properties_json(ns, message_handler, goto_functions);
+    show_properties_json(ns, ui_message_handler, goto_functions);
   else
     for(const auto &fct : goto_functions.function_map)
-      show_properties(ns, fct.first, message_handler, ui, fct.second.body);
+      show_properties(ns, fct.first, ui_message_handler, ui, fct.second.body);
 }
 
 void show_properties(
   const goto_modelt &goto_model,
-  message_handlert &message_handler,
-  ui_message_handlert::uit ui)
+  ui_message_handlert &ui_message_handler)
 {
+  ui_message_handlert::uit ui = ui_message_handler.get_ui();
   const namespacet ns(goto_model.symbol_table);
   if(ui == ui_message_handlert::uit::JSON_UI)
-    show_properties_json(ns, message_handler, goto_model.goto_functions);
+    show_properties_json(ns, ui_message_handler, goto_model.goto_functions);
   else
-    show_properties(ns, message_handler, ui, goto_model.goto_functions);
+    show_properties(ns, ui_message_handler, goto_model.goto_functions);
 }

src/goto-programs/show_properties.h

@@ -30,15 +30,12 @@ class message_handlert;
   " --show-properties            show the properties, but don't run analysis\n" // NOLINT(*)
 // clang-format on
 
-void show_properties(
-  const goto_modelt &,
-  message_handlert &message_handler,
-  ui_message_handlert::uit ui);
+void
+show_properties(const goto_modelt &, ui_message_handlert &ui_message_handler);
 
 void show_properties(
   const namespacet &ns,
-  message_handlert &message_handler,
-  ui_message_handlert::uit ui,
+  ui_message_handlert &ui_message_handler,
   const goto_functionst &goto_functions);
 
 /// \brief Returns a source_locationt that corresponds