cprover
|
#include "builtin_factory.h"
#include "ansi_c_internal_additions.h"
#include "ansi_c_parser.h"
#include "ansi_c_typecheck.h"
#include <util/config.h>
#include <util/string_utils.h>
#include <ostream>
#include <sstream>
Go to the source code of this file.
Functions | |
static bool | find_pattern (const std::string &pattern, const char *header_file, std::ostream &out) |
static bool | convert (const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler) |
bool | builtin_factory (const irep_idt &identifier, symbol_tablet &symbol_table, message_handlert &mh) |
Check whether given identifier is a compiler built-in. More... | |
bool builtin_factory | ( | const irep_idt & | identifier, |
symbol_tablet & | symbol_table, | ||
message_handlert & | mh | ||
) |
Check whether given identifier is a compiler built-in.
If so, add declaration to symbol table.
Definition at line 97 of file builtin_factory.cpp.
References configt::ansi_c, ansi_c_internal_additions(), configt::ansi_ct::APPLE, configt::ansi_ct::arch, configt::ansi_ct::ARM, arm_builtin_headers, clang_builtin_headers, configt::ansi_ct::CODEWARRIOR, config, convert(), cprover_builtin_headers, cw_builtin_headers, find_pattern(), configt::ansi_ct::GCC, gcc_builtin_headers_arm, gcc_builtin_headers_generic, gcc_builtin_headers_ia32, gcc_builtin_headers_ia32_2, gcc_builtin_headers_ia32_3, gcc_builtin_headers_ia32_4, gcc_builtin_headers_math, gcc_builtin_headers_mem_string, gcc_builtin_headers_mips, gcc_builtin_headers_omp, gcc_builtin_headers_power, gcc_builtin_headers_tm, gcc_builtin_headers_ubsan, id2string(), configt::ansi_ct::mode, configt::ansi_ct::os, configt::ansi_ct::OS_WIN, and windows_builtin_headers.
Referenced by cpp_typecheckt::builtin_factory(), and c_typecheck_baset::typecheck_side_effect_function_call().
|
static |
Definition at line 41 of file builtin_factory.cpp.
References symbol_table_baset::add(), configt::ansi_c, ansi_c_parser, ansi_c_scanner_init(), ansi_c_typecheck(), ansi_c_parsert::clear(), config, ansi_c_parsert::cpp11, ansi_c_parsert::cpp98, messaget::eom(), messaget::error(), configt::ansi_ct::for_has_scope, ansi_c_parsert::for_has_scope, parsert::in, message_handler, ansi_c_parsert::mode, configt::ansi_ct::mode, ansi_c_parsert::parse(), ansi_c_parsert::parse_tree, parsert::set_file(), messaget::set_message_handler(), and symbol_table_baset::symbols.
Referenced by string_constraint_generatort::add_axioms_for_to_upper_case(), builtin_factory(), bmct::error_trace(), bmc_covert::operator()(), bmc_all_propertiest::report(), clobber_parse_optionst::show_counterexample(), and show_value_sets().
|
static |
Definition at line 21 of file builtin_factory.cpp.
References has_prefix(), and strip_string().
Referenced by builtin_factory().