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

NODISCARD optionalt< 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 147 of file link_goto_model.cpp.

◆ link_goto_model()

NODISCARD optionalt< 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.

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

Definition at line 109 of file link_goto_model.cpp.