23static std::pair<std::optional<replace_symbolt::expr_mapt>,
bool>
27 const std::function<
void(
28 const std::set<irep_idt> &,
85 entry.second.is_static_lifetime && !entry.second.is_type &&
86 !entry.second.is_macro && entry.second.type.id() !=
ID_code &&
112 const std::function<
void(
113 const std::set<irep_idt> &,
133 bool changed =
false;
136 goto_functionst::function_mapt::const_iterator
f_it =
141 f_it->second.body_available())
161 log.warning() <<
"Linking library function '" <<
id <<
"' failed"
177 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
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
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.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
void set_compiled()
Set the symbol's value to "compiled"; to be used once the code-typed value has been converted to a go...
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.
std::optional< 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.
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...
static std::pair< std::optional< 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