link_to_library.cpp File Reference

Library Linking. More...

#include "link_to_library.h"
#include <linking/static_lifetime_init.h>
#include "compute_called_functions.h"
#include "goto_convert_functions.h"
#include "goto_model.h"
#include "link_goto_model.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. 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 23 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 98 of file link_to_library.cpp.