Skip to content

Commit c8702ab

Browse files
committed
CPROVER library linking: move status message to front-end
1 parent c471f72 commit c8702ab

File tree

5 files changed

+5
-5
lines changed

5 files changed

+5
-5
lines changed

src/cbmc/cbmc_parse_options.cpp

+2
Original file line numberDiff line numberDiff line change
@@ -711,6 +711,8 @@ bool cbmc_parse_optionst::process_goto_program(
711711
remove_asm(goto_model);
712712

713713
// add the library
714+
log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
715+
<< eom;
714716
link_to_library(goto_model, log.get_message_handler());
715717

716718
if(options.get_bool_option("string-abstraction"))

src/goto-analyzer/goto_analyzer_parse_options.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -724,6 +724,7 @@ bool goto_analyzer_parse_optionst::process_goto_program(
724724
remove_asm(goto_model);
725725

726726
// add the library
727+
status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
727728
link_to_library(goto_model, ui_message_handler);
728729
#endif
729730

src/goto-diff/goto_diff_parse_options.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -394,6 +394,7 @@ bool goto_diff_parse_optionst::process_goto_program(
394394
remove_asm(goto_model);
395395

396396
// add the library
397+
status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
397398
link_to_library(goto_model, get_message_handler());
398399

399400
// remove function pointers

src/goto-instrument/goto_instrument_parse_options.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -957,6 +957,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
957957
config.ansi_c.defines.push_back("__CPROVER_CUSTOM_BITVECTOR_ANALYSIS");
958958

959959
// add the library
960+
status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
960961
link_to_library(goto_model, get_message_handler());
961962
}
962963

src/goto-programs/link_to_library.cpp

-5
Original file line numberDiff line numberDiff line change
@@ -36,11 +36,6 @@ void link_to_library(
3636
// this needs a fixedpoint, as library functions
3737
// may depend on other library functions
3838

39-
messaget message(message_handler);
40-
41-
message.status() << "Adding CPROVER library ("
42-
<< config.ansi_c.arch << ")" << messaget::eom;
43-
4439
std::set<irep_idt> added_functions;
4540

4641
while(true)

0 commit comments

Comments
 (0)