kept consistency between parse options of cbmc and goto-instrument tools

Display the architecture information if the user intends to add the CPROVER
library for code instrumentation. As a result, the status message is now part
of the link_to_library implementation to avoid redundant code for the respective
library call.

Author: lucasccordeiro

src/cbmc/cbmc_parse_options.cpp

@@ -872,8 +872,6 @@ bool cbmc_parse_optionst::process_goto_program(
     remove_asm(symbol_table, goto_functions);
 
     // add the library
-    status() << "Adding CPROVER library ("
-             << config.ansi_c.arch << ")" << eom;
     link_to_library(symbol_table, goto_functions, ui_message_handler);
 
     if(cmdline.isset("string-abstraction"))

src/clobber/clobber_parse_options.cpp

@@ -368,7 +368,6 @@ bool clobber_parse_optionst::get_goto_program(
 
     // finally add the library
     #if 0
-    status() << "Adding CPROVER library" << eom;
     link_to_library(symbol_table, goto_functions, ui_message_handler);
     #endif
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -378,8 +378,6 @@ bool goto_analyzer_parse_optionst::process_goto_program(
     remove_asm(goto_model);
 
     // add the library
-    status() << "Adding CPROVER library ("
-             << config.ansi_c.arch << ")" << eom;
     link_to_library(goto_model, ui_message_handler);
     #endif
 

src/goto-diff/goto_diff_parse_options.cpp

@@ -480,8 +480,6 @@ bool goto_diff_parse_optionst::process_goto_program(
     remove_asm(symbol_table, goto_functions);
 
     // add the library
-    status() << "Adding CPROVER library ("
-             << config.ansi_c.arch << ")" << eom;
     link_to_library(symbol_table, goto_functions, ui_message_handler);
 
     // remove function pointers

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -983,7 +983,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
        cmdline.isset("custom-bitvector-analysis"))
       config.ansi_c.defines.push_back("__CPROVER_CUSTOM_BITVECTOR_ANALYSIS");
 
-    status() << "Adding CPROVER library" << eom;
+    // add the library
     link_to_library(symbol_table, goto_functions, ui_message_handler);
   }
 

src/goto-programs/link_to_library.cpp

@@ -6,6 +6,8 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include <util/config.h>
+
 #include <ansi-c/cprover_library.h>
 
 #include "link_to_library.h"
@@ -54,6 +56,11 @@ void link_to_library(
   // this needs a fixedpoint, as library functions
   // may depend on other library functions
 
+  messaget message(message_handler);
+
+  message.status() << "Adding CPROVER library ("
+                   << config.ansi_c.arch << ")" << messaget::eom;
+
   std::set<irep_idt> added_functions;
 
   while(true)

src/musketeer/musketeer_parse_options.cpp

@@ -200,7 +200,6 @@ void goto_fence_inserter_parse_optionst::instrument_goto_program(
 
   // we add the library, as some analyses benefit
 
-  status() << "Adding CPROVER library" << eom;
   link_to_library(symbol_table, goto_functions, ui_message_handler);
 
   namespacet ns(symbol_table);

src/symex/symex_parse_options.cpp

@@ -355,7 +355,6 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
   try
   {
     // we add the library
-    status() << "Adding CPROVER library" << eom;
     link_to_library(goto_model, ui_message_handler);
 
     // do partial inlining