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_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  std::ostringstream library_text(prologue);
49 
50  std::size_t count=0;
51 
52  for(const cprover_library_entryt *e = cprover_library; e->function != nullptr;
53  e++)
54  {
55  irep_idt id=e->function;
56 
57  if(functions.find(id)!=functions.end())
58  {
59  symbol_tablet::symbolst::const_iterator old=
60  symbol_table.symbols.find(id);
61 
62  if(old!=symbol_table.symbols.end() &&
63  old->second.value.is_nil())
64  {
65  count++;
66  library_text << e->model << '\n';
67  }
68  }
69  }
70 
71  if(count==0)
72  return std::string();
73  else
74  return library_text.str();
75 }
76 
78  const std::set<irep_idt> &functions,
79  symbol_tablet &symbol_table,
81 {
83  return;
84 
85  std::string library_text;
86 
87  library_text=get_cprover_library_text(functions, symbol_table);
88 
89  add_library(library_text, symbol_table, message_handler);
90 }
91 
93  const std::string &src,
94  symbol_tablet &symbol_table,
96 {
97  if(src.empty())
98  return;
99 
100  std::istringstream in(src);
101 
102  ansi_c_languaget ansi_c_language;
103  ansi_c_language.set_message_handler(message_handler);
104  ansi_c_language.parse(in, "");
105 
106  ansi_c_language.typecheck(symbol_table, "<built-in-library>");
107 }
struct configt::ansi_ct ansi_c
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
static std::string get_cprover_library_text(const std::set< irep_idt > &functions, const symbol_tablet &symbol_table)
bool parse(std::istream &instream, const std::string &path) override
configt config
Definition: config.cpp:23
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)
The symbol table.
Definition: symbol_table.h:19
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
const symbolst & symbols
bool string_abstraction
Definition: config.h:121
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66