CBMC
cprover_library.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_ANSI_C_CPROVER_LIBRARY_H
11 #define CPROVER_ANSI_C_CPROVER_LIBRARY_H
12 
13 #include <set>
14 
15 #include <util/irep.h>
16 
17 class message_handlert;
18 class symbol_table_baset;
19 
21 {
22  const char *function;
23  const char *model;
24 };
25 
26 std::string get_cprover_library_text(
27  const std::set<irep_idt> &functions,
28  const symbol_table_baset &,
29  const struct cprover_library_entryt[],
30  const std::string &prologue,
31  const bool force_load = false);
32 
36 void add_library(
37  const std::string &src,
40  const std::set<irep_idt> &keep = {});
41 
43  const std::set<irep_idt> &functions,
44  const symbol_table_baset &,
47 
52  const std::set<irep_idt> &functions,
53  symbol_table_baset &symbol_table,
54  message_handlert &message_handler);
55 
56 #endif // CPROVER_ANSI_C_CPROVER_LIBRARY_H
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 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 regardl...
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.
The symbol table base class interface.