CBMC
link_to_library.cpp File Reference

Library Linking. More...

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

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_modelgoto model that may contain function calls and symbols with missing function bodies
message_handlermessage handler to report library processing problems
librarygenerator 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.