21 "#line 1 \"gcc_builtin_headers_types.h\"\n"
22 #include "compiler_headers/gcc_builtin_headers_types.inc"
26 "#line 1 \"gcc_builtin_headers_generic.h\"\n"
27 #include "compiler_headers/gcc_builtin_headers_generic.inc"
31 "#line 1 \"gcc_builtin_headers_math.h\"\n"
32 #include "compiler_headers/gcc_builtin_headers_math.inc"
36 "#line 1 \"gcc_builtin_headers_mem_string.h\"\n"
38 #include "compiler_headers/gcc_builtin_headers_mem_string.inc"
42 #include "compiler_headers/gcc_builtin_headers_omp.inc"
46 #include "compiler_headers/gcc_builtin_headers_tm.inc"
50 "#line 1 \"gcc_builtin_headers_ubsan.h\"\n"
51 #include "compiler_headers/gcc_builtin_headers_ubsan.inc"
55 "#line 1 \"gcc_builtin_headers_ia32.h\"\n"
56 #include "compiler_headers/gcc_builtin_headers_ia32.inc"
59 #include "compiler_headers/gcc_builtin_headers_ia32-2.inc"
62 #include "compiler_headers/gcc_builtin_headers_ia32-3.inc"
65 #include "compiler_headers/gcc_builtin_headers_ia32-4.inc"
68 #include "compiler_headers/gcc_builtin_headers_ia32-5.inc"
71 #include "compiler_headers/gcc_builtin_headers_ia32-6.inc"
75 "#line 1 \"gcc_builtin_headers_alpha.h\"\n"
76 #include "compiler_headers/gcc_builtin_headers_alpha.inc"
80 #include "compiler_headers/gcc_builtin_headers_arm.inc"
84 "#line 1 \"gcc_builtin_headers_mips.h\"\n"
85 #include "compiler_headers/gcc_builtin_headers_mips.inc"
89 "#line 1 \"gcc_builtin_headers_power.h\"\n"
90 #include "compiler_headers/gcc_builtin_headers_power.inc"
94 #include "compiler_headers/arm_builtin_headers.inc"
98 #include "compiler_headers/cw_builtin_headers.inc"
102 #include "compiler_headers/clang_builtin_headers.inc"
106 #include "cprover_builtin_headers.inc"
110 #include "compiler_headers/windows_builtin_headers.inc"
115 return std::string(
"const char *" CPROVER_PREFIX "architecture_") +
116 std::string(s) +
"=\"" + value +
"\";\n";
119 template <
typename T>
132 "#line 1 \"<built-in-additions>\"\n"
168 "extern " CPROVER_PREFIX "thread_local const char __PRETTY_FUNCTION__["
180 " short next_avail;\n"
181 " short next_unread;\n"
216 if(support_float16_type)
219 "typedef _Float16 __gcc_v8hf __attribute__((__vector_size__(16)));\n";
221 "typedef _Float16 __gcc_v16hf __attribute__((__vector_size__(32)));\n";
223 "typedef _Float16 __gcc_v32hf __attribute__((__vector_size__(64)));\n";
259 code+=
"typedef long double __float128;\n";
277 code+=
"typedef signed __int128 __int128_t;\n"
278 "typedef unsigned __int128 __uint128_t;\n";
284 code +=
"int __assume(int);\n";
304 code +=
"#line 1 \"<builtin-architecture-strings>\"\n";
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
static std::string architecture_string(const std::string &value, const char *s)
const char gcc_builtin_headers_types[]
const char cprover_builtin_headers[]
const char gcc_builtin_headers_ia32[]
const char gcc_builtin_headers_ia32_2[]
const char gcc_builtin_headers_ia32_5[]
const char gcc_builtin_headers_ubsan[]
void ansi_c_internal_additions(std::string &code, bool support_float16_type)
const char windows_builtin_headers[]
const char gcc_builtin_headers_mem_string[]
const char gcc_builtin_headers_ia32_4[]
const char gcc_builtin_headers_generic[]
const char gcc_builtin_headers_tm[]
const char cw_builtin_headers[]
const char gcc_builtin_headers_math[]
const char gcc_builtin_headers_arm[]
const char gcc_builtin_headers_ia32_6[]
const char gcc_builtin_headers_mips[]
const char clang_builtin_headers[]
const char gcc_builtin_headers_alpha[]
const char arm_builtin_headers[]
const char gcc_builtin_headers_omp[]
const char gcc_builtin_headers_ia32_3[]
const char gcc_builtin_headers_power[]
void ansi_c_architecture_strings(std::string &code)
std::string c_type_as_string(const irep_idt &c_type)
signedbv_typet signed_size_type()
mp_integer max_malloc_size() const
The maximum allocation size is determined by the number of bits that are left in the pointer of width...
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
const std::string integer2string(const mp_integer &n, unsigned base)
#define INITIALIZE_FUNCTION
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
std::size_t long_double_width
static std::string os_to_string(ost)
std::size_t pointer_width
ieee_floatt::rounding_modet rounding_mode
std::size_t wchar_t_width
std::size_t memory_operand_size
std::size_t long_long_int_width
std::size_t long_int_width
std::size_t short_int_width