CBMC
cprover_library.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Michael Tautschnig
6 
7 \*******************************************************************/
8 
9 #include "cprover_library.h"
10 
11 #include <sstream>
12 
13 #include <util/config.h>
14 
15 #include <ansi-c/cprover_library.h>
16 
17 static std::string get_cprover_library_text(
18  const std::set<irep_idt> &functions,
19  const symbol_tablet &symbol_table)
20 {
21  std::ostringstream library_text;
22 
23  library_text << "#line 1 \"<builtin-library>\"\n"
24  << "#undef inline\n";
25 
26  // cprover_library.inc may not have been generated when running Doxygen, thus
27  // make Doxygen skip this part
29  const struct cprover_library_entryt cprover_library[] =
30 #include "cprover_library.inc"
31  ; // NOLINT(whitespace/semicolon)
33 
35  functions, symbol_table, cprover_library, library_text.str());
36 }
37 
39  const std::set<irep_idt> &functions,
40  symbol_tablet &symbol_table,
41  message_handlert &message_handler)
42 {
44  return;
45 
46  const std::string library_text =
47  get_cprover_library_text(functions, symbol_table);
48 
49  add_library(library_text, symbol_table, message_handler);
50 }
symbol_tablet
The symbol table.
Definition: symbol_table.h:13
configt::ansi_c
struct configt::ansi_ct ansi_c
configt::ansi_ct::libt::LIB_NONE
@ LIB_NONE
cprover_library_entryt
Definition: cprover_library.h:20
message_handlert
Definition: message.h:27
config
configt config
Definition: config.cpp:25
get_cprover_library_text
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: cprover_library.cpp:59
add_library
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.
Definition: cprover_library.cpp:112
config.h
configt::ansi_ct::lib
libt lib
Definition: config.h:261
cprover_library.h
cprover_cpp_library_factory
void cprover_cpp_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:38