25 const std::function<
void(
26 const std::set<irep_idt> &,
73 entry.second.is_static_lifetime && !entry.second.is_type &&
74 !entry.second.is_macro && entry.second.type.id() !=
ID_code &&
100 const std::function<
void(
101 const std::set<irep_idt> &,
121 bool changed =
false;
124 goto_functionst::function_mapt::const_iterator
f_it =
129 f_it->second.body_available())
149 log.warning() <<
"Linking library function '" <<
id <<
"' failed"
165 if(!object_type_updates.empty())
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
function_mapt function_map
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
Class that provides messages with a built-in verbosity 'level'.
std::unordered_map< irep_idt, exprt > expr_mapt
const symbolst & symbols
Read-only field, used to look up symbols given their names.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
std::unordered_set< irep_idt > compute_called_functions(const goto_functionst &goto_functions)
computes the functions that are (potentially) called
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
void finalize_linking(goto_modelt &dest, const replace_symbolt::expr_mapt &type_updates)
Apply type_updates to dest, where type_updates were constructed from one or more calls to link_goto_m...
optionalt< replace_symbolt::expr_mapt > link_goto_model(goto_modelt &dest, goto_modelt &&src, message_handlert &message_handler)
Link goto model src into goto model dest, invalidating src in this process.
static std::pair< optionalt< replace_symbolt::expr_mapt >, bool > add_one_function(goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, const symbol_tablet &, symbol_tablet &, message_handlert &)> &library, const irep_idt &missing_function)
Try to add missing_function from library to goto_model.
void link_to_library(goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, const symbol_tablet &, symbol_tablet &, message_handlert &)> &library)
Complete missing function definitions using the library.
void recreate_initialize_function(goto_modelt &goto_model, message_handlert &message_handler)
Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto m...
#define INITIALIZE_FUNCTION