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 #include <util/symbol_table.h>
15 
16 #include "ansi_c_language.h"
17 
18 static std::string get_cprover_library_text(
19  const std::set<irep_idt> &functions,
20  const symbol_tablet &symbol_table)
21 {
22  std::ostringstream library_text;
23 
24  library_text <<
25  "#line 1 \"<builtin-library>\"\n"
26  "#undef inline\n";
27 
29  library_text << "#define " CPROVER_PREFIX "STRING_ABSTRACTION\n";
30 
31  // cprover_library.inc may not have been generated when running Doxygen, thus
32  // make Doxygen skip this part
34  const struct cprover_library_entryt cprover_library[] =
35 #include "cprover_library.inc"
36  ; // NOLINT(whitespace/semicolon)
38 
40  functions, symbol_table, cprover_library, library_text.str());
41 }
42 
44  const std::set<irep_idt> &functions,
45  const symbol_tablet &symbol_table,
46  const struct cprover_library_entryt cprover_library[],
47  const std::string &prologue)
48 {
49  // the default mode is ios_base::out which means subsequent write to the
50  // stream will overwrite the original content
51  std::ostringstream library_text(prologue, std::ios_base::ate);
52 
53  std::size_t count=0;
54 
55  for(const cprover_library_entryt *e = cprover_library; e->function != nullptr;
56  e++)
57  {
58  irep_idt id=e->function;
59 
60  if(functions.find(id)!=functions.end())
61  {
62  symbol_tablet::symbolst::const_iterator old=
63  symbol_table.symbols.find(id);
64 
65  if(old!=symbol_table.symbols.end() &&
66  old->second.value.is_nil())
67  {
68  count++;
69  library_text << e->model << '\n';
70  }
71  }
72  }
73 
74  if(count==0)
75  return std::string();
76  else
77  return library_text.str();
78 }
79 
81  const std::set<irep_idt> &functions,
82  symbol_tablet &symbol_table,
83  message_handlert &message_handler)
84 {
86  return;
87 
88  std::string library_text;
89 
90  library_text=get_cprover_library_text(functions, symbol_table);
91 
92  add_library(library_text, symbol_table, message_handler);
93 }
94 
96  const std::string &src,
97  symbol_tablet &symbol_table,
98  message_handlert &message_handler)
99 {
100  if(src.empty())
101  return;
102 
103  std::istringstream in(src);
104 
105  ansi_c_languaget ansi_c_language;
106  ansi_c_language.set_message_handler(message_handler);
107  ansi_c_language.parse(in, "");
108 
109  ansi_c_language.typecheck(symbol_table, "<built-in-library>");
110 }
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)
static std::string get_cprover_library_text(const std::set< irep_idt > &functions, const symbol_tablet &symbol_table)
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
bool parse(std::istream &instream, const std::string &path) override
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:179
const symbolst & symbols
Read-only field, used to look up symbols given their names.
The symbol table.
Definition: symbol_table.h:14
configt config
Definition: config.cpp:25
#define CPROVER_PREFIX
bool string_abstraction
Definition: config.h:210
Author: Diffblue Ltd.