#include "cprover_library.h"
#include <util/config.h>
#include <util/cprover_prefix.h>
#include <util/symbol_table_base.h>
#include "ansi_c_language.h"
#include <sstream>

Include dependency graph for cprover_library.cpp:

Functions
static std::string	get_cprover_library_text (const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, const bool force_load)

std::string	get_cprover_library_text (const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, const struct cprover_library_entryt cprover_library[], const std::string &prologue, const bool force_load)

void	cprover_c_library_factory (const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)

void	add_library (const std::string &src, symbol_table_baset &symbol_table, message_handlert &message_handler, const std::set< irep_idt > &keep)
	Parses and typechecks the given src and adds its contents to the symbol table. More...

void	cprover_c_library_factory_force_load (const std::set< irep_idt > &functions, symbol_table_baset &symbol_table, message_handlert &message_handler)
	Load the requested function symbols from the cprover library and add them to the symbol table regardless of the library config flags and usage. More...

Function Documentation

◆ add_library()

void add_library	(	const std::string &	src,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler,
		const std::set< irep_idt > &	keep = `{}`
	)

Parses and typechecks the given src and adds its contents to the symbol table.

Symbols with names found in keep will survive the symbol table cleanup pass and be found in the symbol_table.

Definition at line 114 of file cprover_library.cpp.

◆ cprover_c_library_factory()

void cprover_c_library_factory	(	const std::set< irep_idt > &	functions,
		const symbol_table_baset &	symbol_table,
		symbol_table_baset &	dest_symbol_table,
		message_handlert &	message_handler
	)

Definition at line 99 of file cprover_library.cpp.

◆ cprover_c_library_factory_force_load()

void cprover_c_library_factory_force_load	(	const std::set< irep_idt > &	functions,
		symbol_table_baset &	symbol_table,
		message_handlert &	message_handler
	)

Load the requested function symbols from the cprover library and add them to the symbol table regardless of the library config flags and usage.

Definition at line 132 of file cprover_library.cpp.

◆ get_cprover_library_text() [1/2]

static std::string get_cprover_library_text	(	const std::set< irep_idt > &	functions,
		const symbol_table_baset &	symbol_table,
		const bool	force_load
	)

static

Definition at line 19 of file cprover_library.cpp.

◆ get_cprover_library_text() [2/2]

std::string get_cprover_library_text	(	const std::set< irep_idt > &	functions,
		const symbol_table_baset &	symbol_table,
		const struct cprover_library_entryt	cprover_library[],
		const std::string &	prologue,
		const bool	force_load
	)