cprover
link_to_library.h File Reference

Library Linking. More...

#include <functional>
#include <set>
#include <util/deprecate.h>
#include <util/irep.h>
+ Include dependency graph for link_to_library.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions

void link_to_library (symbol_tablet &, goto_functionst &, message_handlert &, const std::function< void(const std::set< irep_idt > &, symbol_tablet &, message_handlert &)> &)
 Complete missing function definitions using the library. More...
 
void link_to_library (goto_modelt &, message_handlert &, const std::function< void(const std::set< irep_idt > &, symbol_tablet &, message_handlert &)> &)
 Complete missing function definitions using the library. More...
 

Detailed Description

Library Linking.

Definition in file link_to_library.h.

Function Documentation

◆ link_to_library() [1/2]

void link_to_library ( goto_modelt goto_model,
message_handlert message_handler,
const std::function< void(const std::set< irep_idt > &, 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 for a given set of symbol names that have no body.

Definition at line 24 of file link_to_library.cpp.

◆ link_to_library() [2/2]

void link_to_library ( symbol_tablet symbol_table,
goto_functionst goto_functions,
message_handlert message_handler,
const std::function< void(const std::set< irep_idt > &, symbol_tablet &, message_handlert &)> &  library 
)

Complete missing function definitions using the library.

Deprecated:
SINCE(2019, 2, 28, "Use link_to_library(goto_model, ...) instead")
Parameters
symbol_tablesymbol table that may contain symbols with missing function bodies
goto_functionsgoto functions that may contain function calls with missing function bodies
message_handlermessage handler to report library processing problems
librarygenerator function that produces function definitions for a given set of symbol names that have no body.

Definition at line 98 of file link_to_library.cpp.