cprover
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)
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.
std::optional< replace_symbolt::expr_maptlink_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()

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

◆ rename_symbols_in_function()

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.