18 const std::set<irep_idt> &functions,
21 std::ostringstream library_text;
24 "#line 1 \"<builtin-library>\"\n" 28 library_text <<
"#define __CPROVER_STRING_ABSTRACTION\n";
34 #include "cprover_library.inc" 39 functions, symbol_table, cprover_library, library_text.str());
43 const std::set<irep_idt> &functions,
46 const std::string &prologue)
48 std::ostringstream library_text(prologue);
57 if(functions.find(
id)!=functions.end())
59 symbol_tablet::symbolst::const_iterator old=
62 if(old!=symbol_table.
symbols.end() &&
63 old->second.value.is_nil())
66 library_text << e->model <<
'\n';
74 return library_text.str();
78 const std::set<irep_idt> &functions,
85 std::string library_text;
93 const std::string &src,
100 std::istringstream in(src);
104 ansi_c_language.
parse(in,
"");
106 ansi_c_language.
typecheck(symbol_table,
"<built-in-library>");
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
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)
virtual void set_message_handler(message_handlert &_message_handler)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
goto_programt coverage_criteriont message_handlert & message_handler