Skip to content

Commit

Permalink
Rename add_cprover_X_library to cprover_X_library_factory
Browse files Browse the repository at this point in the history
This name more clearly describes what these functions do.
  • Loading branch information
tautschnig committed Jun 8, 2018
1 parent 1201ffe commit 4edecbc
Show file tree
Hide file tree
Showing 8 changed files with 17 additions and 12 deletions.
2 changes: 1 addition & 1 deletion src/ansi-c/cprover_library.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ std::string get_cprover_library_text(
return library_text.str();
}

void add_cprover_c_library(
void cprover_c_library_factory(
const std::set<irep_idt> &functions,
symbol_tablet &symbol_table,
message_handlert &message_handler)
Expand Down
2 changes: 1 addition & 1 deletion src/ansi-c/cprover_library.h
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ void add_library(
symbol_tablet &,
message_handlert &);

void add_cprover_c_library(
void cprover_c_library_factory(
const std::set<irep_idt> &functions,
symbol_tablet &,
message_handlert &);
Expand Down
4 changes: 2 additions & 2 deletions src/cbmc/cbmc_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -717,9 +717,9 @@ bool cbmc_parse_optionst::process_goto_program(
log.status() << "Adding CPROVER library (" << config.ansi_c.arch << ")"
<< eom;
link_to_library(
goto_model, log.get_message_handler(), add_cprover_cpp_library);
goto_model, log.get_message_handler(), cprover_cpp_library_factory);
link_to_library(
goto_model, log.get_message_handler(), add_cprover_c_library);
goto_model, log.get_message_handler(), cprover_c_library_factory);

if(options.get_bool_option("string-abstraction"))
string_instrumentation(goto_model, log.get_message_handler());
Expand Down
2 changes: 1 addition & 1 deletion src/cpp/cprover_library.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ static std::string get_cprover_library_text(
functions, symbol_table, cprover_library, library_text.str());
}

void add_cprover_cpp_library(
void cprover_cpp_library_factory(
const std::set<irep_idt> &functions,
symbol_tablet &symbol_table,
message_handlert &message_handler)
Expand Down
2 changes: 1 addition & 1 deletion src/cpp/cprover_library.h
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ Author: Michael Tautschnig
class message_handlert;
class symbol_tablet;

void add_cprover_cpp_library(
void cprover_cpp_library_factory(
const std::set<irep_idt> &functions,
symbol_tablet &,
message_handlert &);
Expand Down
5 changes: 3 additions & 2 deletions src/goto-analyzer/goto_analyzer_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -729,8 +729,9 @@ bool goto_analyzer_parse_optionst::process_goto_program(

// add the library
status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
link_to_library(goto_model, ui_message_handler, add_cprover_cpp_library);
link_to_library(goto_model, ui_message_handler, add_cprover_c_library);
link_to_library(
goto_model, ui_message_handler, cprover_cpp_library_factory);
link_to_library(goto_model, ui_message_handler, cprover_c_library_factory);
#endif

// remove function pointers
Expand Down
6 changes: 4 additions & 2 deletions src/goto-diff/goto_diff_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -398,8 +398,10 @@ bool goto_diff_parse_optionst::process_goto_program(

// add the library
status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
link_to_library(goto_model, get_message_handler(), add_cprover_cpp_library);
link_to_library(goto_model, get_message_handler(), add_cprover_c_library);
link_to_library(
goto_model, get_message_handler(), cprover_cpp_library_factory);
link_to_library(
goto_model, get_message_handler(), cprover_c_library_factory);

// remove function pointers
status() << "Removal of function pointers and virtual functions" << eom;
Expand Down
6 changes: 4 additions & 2 deletions src/goto-instrument/goto_instrument_parse_options.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -961,8 +961,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()

// add the library
status() << "Adding CPROVER library (" << config.ansi_c.arch << ")" << eom;
link_to_library(goto_model, get_message_handler(), add_cprover_cpp_library);
link_to_library(goto_model, get_message_handler(), add_cprover_c_library);
link_to_library(
goto_model, get_message_handler(), cprover_cpp_library_factory);
link_to_library(
goto_model, get_message_handler(), cprover_c_library_factory);
}

// now do full inlining, if requested
Expand Down

0 comments on commit 4edecbc

Please sign in to comment.