Loading...

Searching...

No Matches

link_goto_model.cpp File Reference

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)

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

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.

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

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

)

static

Definition at line 23 of file link_goto_model.cpp.