Loading...

Searching...

No Matches

link_to_library.cpp File Reference

Library Linking. More...

#include "link_to_library.h"
#include <goto-programs/compute_called_functions.h>
#include <goto-programs/goto_model.h>
#include <goto-programs/link_goto_model.h>
#include <linking/static_lifetime_init.h>
#include "goto_convert_functions.h"

+ Include dependency graph for link_to_library.cpp:

[フレーム]

Go to the source code of this file.

Functions

static std::pair< std::optional< replace_symbolt::expr_mapt >, bool > add_one_function (goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, const symbol_tablet &, symbol_tablet &, message_handlert &)> &library, const irep_idt &missing_function)

Try to add missing_function from library to goto_model.

void link_to_library (goto_modelt &goto_model, message_handlert &message_handler, const std::function< void(const std::set< irep_idt > &, const symbol_tablet &, symbol_tablet &, message_handlert &)> &library)

Complete missing function definitions using the library.

Detailed Description

Library Linking.

Definition in file link_to_library.cpp.

Function Documentation

◆ add_one_function()

static std::pair< std::optional< replace_symbolt::expr_mapt >, bool > add_one_function ( goto_modelt & goto_model,

message_handlert & message_handler,

const std::function< void(const std::set< irep_idt > &, const symbol_tablet &, symbol_tablet &, message_handlert &)> & library,

const irep_idt & missing_function

)

static

Try to add missing_function from library to goto_model.

Definition at line 24 of file link_to_library.cpp.

◆ link_to_library()

void link_to_library ( goto_modelt & goto_model,

message_handlert & message_handler,

const std::function< void(const std::set< irep_idt > &, const symbol_tablet &, symbol_tablet &, message_handlert &)> & library

)

Complete missing function definitions using the library.

Parameters: goto_model goto model that may contain function calls and symbols with missing function bodies

message_handler message handler to report library processing problems

library generator function that produces function definitions (in the symbol table that is the third parameter) for a given set of symbol names (first parameter) that have no body in the source symbol table (second parameter).

Definition at line 109 of file link_to_library.cpp.