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 <util/config.h>
12#include <util/cprover_prefix.h>
14
15#include "ansi_c_language.h"
16
17#include <sstream>
18
19static std::string get_cprover_library_text(
20 const std::set<irep_idt> &functions,
21 const symbol_table_baset &symbol_table,
22 const bool force_load)
23{
24 std::ostringstream library_text;
25
26 library_text << "#line 1 \"<built-in-additions>\"\n"
27 "#define " CPROVER_PREFIX "malloc_failure_mode "
28 << std::to_string(config.ansi_c.malloc_failure_mode)
29 << "\n"
30 "#define " CPROVER_PREFIX "malloc_failure_mode_return_null "
32 << "\n"
33 "#define " CPROVER_PREFIX
34 "malloc_failure_mode_assert_then_assume "
35 << std::to_string(
37 << "\n"
38 "#define " CPROVER_PREFIX "malloc_may_fail "
39 << std::to_string(config.ansi_c.malloc_may_fail) << "\n";
40
41 library_text <<
42 "#line 1 \"<builtin-library>\"\n"
43 "#undef inline\n";
44
46 library_text << "#define " CPROVER_PREFIX "STRING_ABSTRACTION\n";
47
48 // cprover_library.inc may not have been generated when running Doxygen, thus
49 // make Doxygen skip this part
51 const struct cprover_library_entryt cprover_library[] =
52#include "cprover_library.inc" // IWYU pragma: keep
53 ; // NOLINT(whitespace/semicolon)
55
57 functions, symbol_table, cprover_library, library_text.str(), force_load);
58}
59
61 const std::set<irep_idt> &functions,
62 const symbol_table_baset &symbol_table,
63 const struct cprover_library_entryt cprover_library[],
64 const std::string &prologue,
65 const bool force_load)
66{
67 // the default mode is ios_base::out which means subsequent write to the
68 // stream will overwrite the original content
69 std::ostringstream library_text(prologue, std::ios_base::ate);
70
71 std::size_t count=0;
72
73 for(const cprover_library_entryt *e = cprover_library; e->function != nullptr;
74 e++)
75 {
76 irep_idt id=e->function;
77
78 if(functions.find(id)!=functions.end())
79 {
80 symbol_table_baset::symbolst::const_iterator old =
81 symbol_table.symbols.find(id);
82
83 if(
84 force_load ||
85 (old != symbol_table.symbols.end() && old->second.value.is_nil()))
86 {
87 count++;
88 library_text << e->model << '\n';
89 }
90 }
91 }
92
93 if(count==0)
94 return std::string();
95 else
96 return library_text.str();
97}
98
100 const std::set<irep_idt> &functions,
101 const symbol_table_baset &symbol_table,
102 symbol_table_baset &dest_symbol_table,
103 message_handlert &message_handler)
104{
106 return;
107
108 std::string library_text =
109 get_cprover_library_text(functions, symbol_table, false);
110
111 add_library(library_text, dest_symbol_table, message_handler);
112}
113
115 const std::string &src,
116 symbol_table_baset &symbol_table,
117 message_handlert &message_handler,
118 const std::set<irep_idt> &keep)
119{
120 if(src.empty())
121 return;
122
123 std::istringstream in(src);
124
125 ansi_c_languaget ansi_c_language;
126 ansi_c_language.set_message_handler(message_handler);
127 ansi_c_language.parse(in, "");
128
129 ansi_c_language.typecheck(symbol_table, "<built-in-library>", true, keep);
130}
131
133 const std::set<irep_idt> &functions,
134 symbol_table_baset &symbol_table,
135 message_handlert &message_handler)
136{
137 std::string library_text =
138 get_cprover_library_text(functions, symbol_table, true);
139 add_library(library_text, symbol_table, message_handler, functions);
140}
static std::string get_cprover_library_text(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, const bool force_load)
void add_library(const std::string &src, symbol_table_baset &symbol_table, message_handlert &message_handler, const std::set< irep_idt > &keep)
Parses and typechecks the given src and adds its contents to the symbol table.
void cprover_c_library_factory_force_load(const std::set< irep_idt > &functions, symbol_table_baset &symbol_table, message_handlert &message_handler)
Load the requested function symbols from the cprover library and add them to the symbol table regardl...
void cprover_c_library_factory(const std::set< irep_idt > &functions, const symbol_table_baset &symbol_table, symbol_table_baset &dest_symbol_table, message_handlert &message_handler)
configt config
Definition config.cpp:25
bool parse(std::istream &instream, const std::string &path) override
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
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:39
virtual void set_message_handler(message_handlert &_message_handler)
Definition message.h:179
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.
#define CPROVER_PREFIX
@ malloc_failure_mode_return_null
Definition config.h:281
@ malloc_failure_mode_assert_then_assume
Definition config.h:282
bool malloc_may_fail
Definition config.h:276
bool string_abstraction
Definition config.h:275
malloc_failure_modet malloc_failure_mode
Definition config.h:285
Author: Diffblue Ltd.