cprover_library.cpp File Reference

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

Include dependency graph for cprover_library.cpp:

Go to the source code of this file.

Functions
static std::string	get_cprover_library_text (const std::set< irep_idt > &functions, const symbol_tablet &symbol_table, const bool force_load)
std::string	get_cprover_library_text (const std::set< irep_idt > &functions, const symbol_tablet &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, symbol_tablet &symbol_table, message_handlert &message_handler)
void	add_library (const std::string &src, symbol_tablet &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_tablet &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_tablet &	,
		message_handlert &	,
		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 112 of file cprover_library.cpp.

cprover_c_library_factory()

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

Definition at line 98 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_tablet &	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 130 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_tablet &  symbol_table, const bool  force_load  )

static

Definition at line 18 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_tablet &	symbol_table,
		const struct cprover_library_entryt	cprover_library[],
		const std::string &	prologue,
		const bool	force_load
	)

Definition at line 59 of file cprover_library.cpp.