CBMC
|
Read Goto Programs. More...
#include <util/replace_symbol.h>
Go to the source code of this file.
Functions | |
std::optional< replace_symbolt::expr_mapt > | link_goto_model (goto_modelt &dest, goto_modelt &&src, message_handlert &) |
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... | |
Read Goto Programs.
Definition in file link_goto_model.h.
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.
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.