22 #include "cprover_library.inc" 26 const std::set<irep_idt> &functions,
29 std::ostringstream library_text;
32 "#line 1 \"<builtin-library>\"\n" 36 library_text <<
"#define __CPROVER_STRING_ABSTRACTION\n";
46 if(functions.find(
id)!=functions.end())
48 symbol_tablet::symbolst::const_iterator old=
51 if(old!=symbol_table.
symbols.end() &&
52 old->second.value.is_nil())
55 library_text << e->model <<
'\n';
63 return library_text.str();
67 const std::set<irep_idt> &functions,
74 std::string library_text;
78 add_library(library_text, symbol_table, message_handler);
82 const std::string &src,
89 std::istringstream in(src);
93 ansi_c_language.
parse(in,
"");
95 ansi_c_language.
typecheck(symbol_table,
"<built-in-library>");
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
virtual void set_message_handler(message_handlert &_message_handler)
struct cprover_library_entryt cprover_library[]
void add_library(const std::string &src, symbol_tablet &symbol_table, message_handlert &message_handler)
void add_cprover_library(const std::set< irep_idt > &functions, symbol_tablet &symbol_table, message_handlert &message_handler)