CBMC
|
Link Goto Programs. More...
#include "link_goto_model.h"
#include <linking/linking_class.h>
#include <util/message.h>
#include <util/rename_symbol.h>
#include <util/symbol.h>
#include "goto_model.h"
#include <unordered_set>
Go to the source code of this file.
Functions | |
static void | rename_symbols_in_function (goto_functionst::goto_functiont &function, const rename_symbolt &rename_symbol) |
static bool | link_functions (symbol_tablet &dest_symbol_table, goto_functionst &dest_functions, const symbol_tablet &src_symbol_table, goto_functionst &src_functions, const rename_symbolt &rename_dest_symbol, const rename_symbolt &rename_src_symbol, const std::unordered_set< irep_idt > &weak_symbols) |
Link a set of goto functions, considering weak symbols and symbol renaming. More... | |
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. More... | |
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_model . More... | |
Link Goto Programs.
Definition in file link_goto_model.cpp.
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_model
.
Definition at line 164 of file link_goto_model.cpp.
|
static |
Link a set of goto functions, considering weak symbols and symbol renaming.
Definition at line 45 of file link_goto_model.cpp.
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.
Linking may require updates to object types contained in dest
, which need to be applied using finalize_linking.
Definition at line 125 of file link_goto_model.cpp.
|
static |
Definition at line 23 of file link_goto_model.cpp.