20 const std::set<irep_idt> &functions,
22 const bool force_load)
24 std::ostringstream library_text;
26 library_text <<
"#line 1 \"<built-in-additions>\"\n"
28 << std::to_string(
config.ansi_c.malloc_failure_mode)
31 << std::to_string(
config.ansi_c.malloc_failure_mode_return_null)
34 "malloc_failure_mode_assert_then_assume "
36 config.ansi_c.malloc_failure_mode_assert_then_assume)
39 << std::to_string(
config.ansi_c.malloc_may_fail) <<
"\n";
42 "#line 1 \"<builtin-library>\"\n"
45 if(
config.ansi_c.string_abstraction)
48 if(
config.ansi_c.dfcc_debug_lib)
51 if(
config.ansi_c.simple_invalid_pointer_model)
53 "DFCC_SIMPLE_INVALID_POINTER_MODEL\n";
59#include "cprover_library.inc"
64 functions, symbol_table, cprover_library, library_text.str(), force_load);
68 const std::set<irep_idt> &functions,
71 const std::string &prologue,
72 const bool force_load)
76 std::ostringstream library_text(prologue, std::ios_base::ate);
85 if(functions.find(
id)!=functions.end())
87 symbol_table_baset::symbolst::const_iterator old =
92 (old != symbol_table.
symbols.end() && old->second.value.is_nil()))
95 library_text << e->model <<
'\n';
101 return std::string();
103 return library_text.str();
107 const std::set<irep_idt> &functions,
115 std::string library_text =
118 add_library(library_text, dest_symbol_table, message_handler);
122 const std::string &src,
125 const std::set<irep_idt> &keep)
130 std::istringstream in(src);
133 ansi_c_language.
parse(in,
"", message_handler);
136 symbol_table,
"<built-in-library>", message_handler,
true, keep);
140 const std::set<irep_idt> &functions,
144 std::string library_text =
146 add_library(library_text, symbol_table, message_handler, functions);
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)
bool typecheck(symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler, const bool keep_file_local) override
typecheck without removing specified entries from the symbol table
bool parse(std::istream &instream, const std::string &path, message_handlert &message_handler) override
The symbol table base class interface.
const symbolst & symbols
Read-only field, used to look up symbols given their names.