41 message.
status() <<
"Adding CPROVER library (" 44 std::set<irep_idt> added_functions;
48 std::set<irep_idt> called_functions;
53 std::set<irep_idt> missing_functions;
55 for(
const auto &
id : called_functions)
57 goto_functionst::function_mapt::const_iterator
61 f_it->second.body_available())
65 else if(added_functions.find(
id)!=added_functions.end())
70 missing_functions.insert(
id);
74 if(missing_functions.empty())
80 for(
const auto &
id : missing_functions)
83 goto_convert(
id, symbol_table, goto_functions, message_handler);
85 added_functions.insert(
id);
struct configt::ansi_ct ansi_c
void goto_convert(const codet &code, symbol_tablet &symbol_table, goto_programt &dest, message_handlert &message_handler)
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler)
symbol_tablet symbol_table
static mstreamt & eom(mstreamt &m)
function_mapt function_map
Goto Programs with Functions.
void compute_called_functions(const goto_functionst &goto_functions, std::set< irep_idt > &functions)
computes the functions that are (potentially) called
void add_cprover_library(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
goto_functionst goto_functions