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 
18 {
19  const char *function;
20  const char *model;
21 } cprover_library[]=
22 #include "cprover_library.inc"
23 ; // NOLINT(whitespace/semicolon)
24 
26  const std::set<irep_idt> &functions,
27  const symbol_tablet &symbol_table)
28 {
29  std::ostringstream library_text;
30 
31  library_text <<
32  "#line 1 \"<builtin-library>\"\n"
33  "#undef inline\n";
34 
36  library_text << "#define __CPROVER_STRING_ABSTRACTION\n";
37 
38  std::size_t count=0;
39 
41  e->function!=nullptr;
42  e++)
43  {
44  irep_idt id=e->function;
45 
46  if(functions.find(id)!=functions.end())
47  {
48  symbol_tablet::symbolst::const_iterator old=
49  symbol_table.symbols.find(id);
50 
51  if(old!=symbol_table.symbols.end() &&
52  old->second.value.is_nil())
53  {
54  count++;
55  library_text << e->model << '\n';
56  }
57  }
58  }
59 
60  if(count==0)
61  return std::string();
62  else
63  return library_text.str();
64 }
65 
67  const std::set<irep_idt> &functions,
68  symbol_tablet &symbol_table,
69  message_handlert &message_handler)
70 {
72  return;
73 
74  std::string library_text;
75 
76  library_text=get_cprover_library_text(functions, symbol_table);
77 
78  add_library(library_text, symbol_table, message_handler);
79 }
80 
82  const std::string &src,
83  symbol_tablet &symbol_table,
84  message_handlert &message_handler)
85 {
86  if(src.empty())
87  return;
88 
89  std::istringstream in(src);
90 
91  ansi_c_languaget ansi_c_language;
92  ansi_c_language.set_message_handler(message_handler);
93  ansi_c_language.parse(in, "");
94 
95  ansi_c_language.typecheck(symbol_table, "<built-in-library>");
96 }
std::string get_cprover_library_text(const std::set< irep_idt > &functions, const symbol_tablet &symbol_table)
struct configt::ansi_ct ansi_c
bool typecheck(symbol_tablet &symbol_table, const std::string &module) override
bool parse(std::istream &instream, const std::string &path) override
configt config
Definition: config.cpp:21
symbolst symbols
Definition: symbol_table.h:57
The symbol table.
Definition: symbol_table.h:52
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
struct cprover_library_entryt cprover_library[]
void add_library(const std::string &src, symbol_tablet &symbol_table, message_handlert &message_handler)
bool string_abstraction
Definition: config.h:120
void add_cprover_library(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)