23 static std::pair<std::optional<replace_symbolt::expr_mapt>,
bool>
27 const std::function<
void(
28 const std::set<irep_idt> &,
77 bool init_required =
false;
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> &,
121 std::set<irep_idt> added_functions;
126 bool need_reinit =
false;
130 std::unordered_set<irep_idt> called_functions =
133 bool changed =
false;
134 for(
const auto &
id : called_functions)
136 goto_functionst::function_mapt::const_iterator f_it =
141 f_it->second.body_available())
145 else if(added_functions.find(
id) != added_functions.end())
152 added_functions.insert(
id);
156 auto updates_opt = one_result.first;
157 need_reinit |= one_result.second;
158 if(!updates_opt.has_value())
161 log.warning() <<
"Linking library function '" <<
id <<
"' failed"
165 object_type_updates.insert(updates_opt->begin(), updates_opt->end());
177 if(!object_type_updates.empty())
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.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
void set_compiled()
Set the symbol's value to "compiled"; to be used once the code-typed value has been converted to a go...
bool is_compiled() const
Returns true iff the the symbol's value has been compiled to a goto program.
exprt value
Initial value of symbol.
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