cprover
cprover_library.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "cprover_library.h"
10 
11 #include <sstream>
12 
13 #include <util/config.h>
14 
15 #include "ansi_c_language.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 <<
24  "#line 1 \"<builtin-library>\"\n"
25  "#undef inline\n";
26 
28  library_text << "#define " CPROVER_PREFIX "STRING_ABSTRACTION\n";
29 
30  // cprover_library.inc may not have been generated when running Doxygen, thus
31  // make Doxygen skip this part
33  const struct cprover_library_entryt cprover_library[] =
34 #include "cprover_library.inc"
35  ; // NOLINT(whitespace/semicolon)
37 
39  functions, symbol_table, cprover_library, library_text.str());
40 }
41 
43  const std::set<irep_idt> &functions,
44  const symbol_tablet &symbol_table,
45  const struct cprover_library_entryt cprover_library[],
46  const std::string &prologue)
47 {
48  // the default mode is ios_base::out which means subsequent write to the
49  // stream will overwrite the original content
50  std::ostringstream library_text(prologue, std::ios_base::ate);
51 
52  std::size_t count=0;
53 
54  for(const cprover_library_entryt *e = cprover_library; e->function != nullptr;
55  e++)
56  {
57  irep_idt id=e->function;
58 
59  if(functions.find(id)!=functions.end())
60  {
61  symbol_tablet::symbolst::const_iterator old=
62  symbol_table.symbols.find(id);
63 
64  if(old!=symbol_table.symbols.end() &&
65  old->second.value.is_nil())
66  {
67  count++;
68  library_text << e->model << '\n';
69  }
70  }
71  }
72 
73  if(count==0)
74  return std::string();
75  else
76  return library_text.str();
77 }
78 
80  const std::set<irep_idt> &functions,
81  symbol_tablet &symbol_table,
82  message_handlert &message_handler)
83 {
85  return;
86 
87  std::string library_text;
88 
89  library_text=get_cprover_library_text(functions, symbol_table);
90 
91  add_library(library_text, symbol_table, message_handler);
92 }
93 
95  const std::string &src,
96  symbol_tablet &symbol_table,
97  message_handlert &message_handler)
98 {
99  if(src.empty())
100  return;
101 
102  std::istringstream in(src);
103 
104  ansi_c_languaget ansi_c_language;
105  ansi_c_language.set_message_handler(message_handler);
106  ansi_c_language.parse(in, "");
107 
108  ansi_c_language.typecheck(symbol_table, "<built-in-library>");
109 }
cprover_library.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
cprover_library_entryt::function
const char * function
Definition: cprover_library.h:20
configt::ansi_c
struct configt::ansi_ct ansi_c
configt::ansi_ct::libt::LIB_NONE
@ LIB_NONE
cprover_library_entryt
Definition: cprover_library.h:19
add_library
void add_library(const std::string &src, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:94
configt::ansi_ct::string_abstraction
bool string_abstraction
Definition: config.h:131
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
message_handlert
Definition: message.h:28
config
configt config
Definition: config.cpp:24
ansi_c_language.h
cprover_c_library_factory
void cprover_c_library_factory(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: cprover_library.cpp:79
ansi_c_languaget::parse
bool parse(std::istream &instream, const std::string &path) override
Definition: ansi_c_language.cpp:52
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
get_cprover_library_text
static std::string get_cprover_library_text(const std::set< irep_idt > &functions, const symbol_tablet &symbol_table)
Definition: cprover_library.cpp:17
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
config.h
ansi_c_languaget::typecheck
bool typecheck(symbol_tablet &symbol_table, const std::string &module, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
Definition: ansi_c_language.cpp:105
configt::ansi_ct::lib
libt lib
Definition: config.h:129
ansi_c_languaget
Definition: ansi_c_language.h:35