CPROVER library linking: move status message to front-end

NathanJPhillips · Jun 8, 2018 · c8702ab · c8702ab
1 parent c471f72
commit c8702ab
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 5 deletions.
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -711,6 +711,8 @@ bool cbmc_parse_optionst::process_goto_program(
     remove_asm(goto_model);
 
     // add the library
+    log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
+                 << eom;
     link_to_library(goto_model, log.get_message_handler());
 
     if(options.get_bool_option("string-abstraction"))

diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -724,6 +724,7 @@ 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
 

diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
@@ -394,6 +394,7 @@ bool goto_diff_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, get_message_handler());
 
     // remove function pointers

diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -957,6 +957,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       config.ansi_c.defines.push_back("__CPROVER_CUSTOM_BITVECTOR_ANALYSIS");
 
     // add the library
+    status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
     link_to_library(goto_model, get_message_handler());
   }
 

diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp
@@ -36,11 +36,6 @@ 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)