link_goto_model.h File Reference

#include <util/nodiscard.h>
#include <util/replace_symbol.h>

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

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()

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

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.