cprover
Loading...
Searching...
No Matches
link_goto_model.h File Reference

Read Goto Programs. More...

Include dependency graph for link_goto_model.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

std::optional< replace_symbolt::expr_maptlink_goto_model (goto_modelt &dest, goto_modelt &&src, message_handlert &)
 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_model.

Detailed Description

Read Goto Programs.

Definition in file link_goto_model.h.

Function Documentation

◆ finalize_linking()

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.

◆ link_goto_model()

std::optional< replace_symbolt::expr_mapt > link_goto_model ( goto_modelt & dest,
goto_modelt && src,
message_handlert & message_handler )
nodiscard

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.

Returns
nullopt if linking fails, else a (possibly empty) collection of replacements to be applied.

Definition at line 125 of file link_goto_model.cpp.