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>

Include dependency graph for link_goto_model.cpp:

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

Detailed Description

Link Goto Programs.

Definition in file link_goto_model.cpp.

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

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
	)

static

Link a set of goto functions, considering weak symbols and symbol renaming.

Definition at line 45 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
	)

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.

◆ rename_symbols_in_function()

static void rename_symbols_in_function	(	goto_functionst::goto_functiont &	function,
		const rename_symbolt &	rename_symbol
	)