cprover
Loading...
Searching...
No Matches
cprover_library.cpp File Reference
#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:

Go to the source code of this file.

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.
 
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.
 

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 121 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 106 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 139 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 )

Definition at line 67 of file cprover_library.cpp.