cprover
Loading...
Searching...
No Matches
cprover_library.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
18static 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 << "#line 1 \"<built-in-additions>\"\n"
25 "#define " CPROVER_PREFIX "malloc_failure_mode "
26 << std::to_string(config.ansi_c.malloc_failure_mode)
27 << "\n"
28 "#define " CPROVER_PREFIX "malloc_failure_mode_return_null "
30 << "\n"
31 "#define " CPROVER_PREFIX
32 "malloc_failure_mode_assert_then_assume "
33 << std::to_string(
35 << "\n"
36 "#define " CPROVER_PREFIX "malloc_may_fail "
37 << std::to_string(config.ansi_c.malloc_may_fail) << "\n";
38
39 library_text <<
40 "#line 1 \"<builtin-library>\"\n"
41 "#undef inline\n";
42
44 library_text << "#define " CPROVER_PREFIX "STRING_ABSTRACTION\n";
45
46 // cprover_library.inc may not have been generated when running Doxygen, thus
47 // make Doxygen skip this part
49 const struct cprover_library_entryt cprover_library[] =
50#include "cprover_library.inc"
51 ; // NOLINT(whitespace/semicolon)
53
55 functions, symbol_table, cprover_library, library_text.str());
56}
57
59 const std::set<irep_idt> &functions,
60 const symbol_tablet &symbol_table,
61 const struct cprover_library_entryt cprover_library[],
62 const std::string &prologue)
63{
64 // the default mode is ios_base::out which means subsequent write to the
65 // stream will overwrite the original content
66 std::ostringstream library_text(prologue, std::ios_base::ate);
67
68 std::size_t count=0;
69
70 for(const cprover_library_entryt *e = cprover_library; e->function != nullptr;
71 e++)
72 {
73 irep_idt id=e->function;
74
75 if(functions.find(id)!=functions.end())
76 {
77 symbol_tablet::symbolst::const_iterator old=
78 symbol_table.symbols.find(id);
79
80 if(old!=symbol_table.symbols.end() &&
81 old->second.value.is_nil())
82 {
83 count++;
84 library_text << e->model << '\n';
85 }
86 }
87 }
88
89 if(count==0)
90 return std::string();
91 else
92 return library_text.str();
93}
94
96 const std::set<irep_idt> &functions,
97 symbol_tablet &symbol_table,
98 message_handlert &message_handler)
99{
101 return;
102
103 std::string library_text;
104
105 library_text=get_cprover_library_text(functions, symbol_table);
106
107 add_library(library_text, symbol_table, message_handler);
108}
109
111 const std::string &src,
112 symbol_tablet &symbol_table,
113 message_handlert &message_handler)
114{
115 if(src.empty())
116 return;
117
118 std::istringstream in(src);
119
120 ansi_c_languaget ansi_c_language;
121 ansi_c_language.set_message_handler(message_handler);
122 ansi_c_language.parse(in, "");
123
124 ansi_c_language.typecheck(symbol_table, "<built-in-library>");
125}
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
@ malloc_failure_mode_return_null
Definition: config.h:254
@ malloc_failure_mode_assert_then_assume
Definition: config.h:255
bool malloc_may_fail
Definition: config.h:249
bool string_abstraction
Definition: config.h:248
malloc_failure_modet malloc_failure_mode
Definition: config.h:258
Author: Diffblue Ltd.