cprover_library.h File Reference

#include <set>
#include <util/irep.h>

Include dependency graph for cprover_library.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	cprover_library_entryt

Functions
std::string	get_cprover_library_text (const std::set< irep_idt > &functions, const symbol_table_baset &, const struct cprover_library_entryt[], const std::string &prologue, const bool force_load=false)
void	add_library (const std::string &src, symbol_table_baset &, message_handlert &, 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 (const std::set< irep_idt > &functions, const symbol_table_baset &, symbol_table_baset &, message_handlert &)
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()

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 = false
	)

Definition at line 60 of file cprover_library.cpp.