14 "# 1 \"gcc_builtin_headers_generic.h\"\n" 15 #include "gcc_builtin_headers_generic.inc" 19 "# 1 \"gcc_builtin_headers_math.h\"\n" 20 #include "gcc_builtin_headers_math.inc" 24 "# 1 \"gcc_builtin_headers_mem_string.h\"\n" 25 #include "gcc_builtin_headers_mem_string.inc" 29 "# 1 \"gcc_builtin_headers_omp.h\"\n" 30 #include "gcc_builtin_headers_omp.inc" 34 "# 1 \"gcc_builtin_headers_tm.h\"\n" 35 #include "gcc_builtin_headers_tm.inc" 39 "# 1 \"gcc_builtin_headers_ubsan.h\"\n" 40 #include "gcc_builtin_headers_ubsan.inc" 44 "# 1 \"gcc_builtin_headers_ia32.h\"\n" 45 #include "gcc_builtin_headers_ia32.inc" 48 #include "gcc_builtin_headers_ia32-2.inc" 51 #include "gcc_builtin_headers_ia32-3.inc" 54 #include "gcc_builtin_headers_ia32-4.inc" 58 "# 1 \"gcc_builtin_headers_alpha.h\"\n" 59 #include "gcc_builtin_headers_alpha.inc" 63 "# 1 \"gcc_builtin_headers_arm.h\"\n" 64 #include "gcc_builtin_headers_arm.inc" 68 "# 1 \"gcc_builtin_headers_mips.h\"\n" 69 #include "gcc_builtin_headers_mips.inc" 73 "# 1 \"gcc_builtin_headers_power.h\"\n" 74 #include "gcc_builtin_headers_power.inc" 78 "# 1 \"arm_builtin_headers.h\"\n" 79 #include "arm_builtin_headers.inc" 83 "# 1 \"cw_builtin_headers.h\"\n" 84 #include "cw_builtin_headers.inc" 88 "# 1 \"clang_builtin_headers.h\"\n" 89 #include "clang_builtin_headers.inc" 94 return std::string(
"const char *__CPROVER_architecture_")+
101 return std::string(
"const int __CPROVER_architecture_")+
103 "="+std::to_string(value)+
";\n";
109 "# 1 \"<built-in-additions>\"\n" 110 "typedef __typeof__(sizeof(int)) __CPROVER_size_t;\n" 111 "void __CPROVER_assume(__CPROVER_bool assumption);\n" 112 "void __VERIFIER_assume(__CPROVER_bool assumption);\n" 114 "void __CPROVER_assert(__CPROVER_bool assertion, const char *description);\n" 115 "__CPROVER_bool __CPROVER_equal();\n" 116 "__CPROVER_bool __CPROVER_same_object(const void *, const void *);\n" 117 "__CPROVER_bool __CPROVER_invalid_pointer(const void *);\n" 118 "__CPROVER_bool __CPROVER_is_zero_string(const void *);\n" 119 "__CPROVER_size_t __CPROVER_zero_string_length(const void *);\n" 120 "__CPROVER_size_t __CPROVER_buffer_size(const void *);\n" 122 "__CPROVER_bool __CPROVER_get_flag(const void *, const char *);\n" 123 "void __CPROVER_set_must(const void *, const char *);\n" 124 "void __CPROVER_clear_must(const void *, const char *);\n" 125 "void __CPROVER_set_may(const void *, const char *);\n" 126 "void __CPROVER_clear_may(const void *, const char *);\n" 127 "void __CPROVER_cleanup(const void *, const void *);\n" 128 "__CPROVER_bool __CPROVER_get_must(const void *, const char *);\n" 129 "__CPROVER_bool __CPROVER_get_may(const void *, const char *);\n" 131 "const unsigned __CPROVER_constant_infinity_uint;\n" 132 "typedef void __CPROVER_integer;\n" 133 "typedef void __CPROVER_rational;\n" 134 "void __CPROVER_initialize(void);\n" 135 "void __CPROVER_input(const char *id, ...);\n" 136 "void __CPROVER_output(const char *id, ...);\n" 137 "void __CPROVER_cover(__CPROVER_bool condition);\n" 140 "void __CPROVER_atomic_begin();\n" 141 "void __CPROVER_atomic_end();\n" 142 "void __CPROVER_fence(const char *kind, ...);\n" 143 "__CPROVER_thread_local unsigned long __CPROVER_thread_id=0;\n" 145 "__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];\n" 146 "unsigned long __CPROVER_next_thread_id=0;\n" 149 "void CBMC_trace(int lvl, const char *event, ...);\n" 152 "unsigned __CPROVER_POINTER_OBJECT(const void *p);\n" 153 "signed __CPROVER_POINTER_OFFSET(const void *p);\n" 154 "__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);\n" 155 "extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];\n" 157 "void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);\n" 160 "void *__CPROVER_malloc(__CPROVER_size_t size);\n" 161 "const void *__CPROVER_deallocated=0;\n" 162 "const void *__CPROVER_dead_object=0;\n" 163 "const void *__CPROVER_malloc_object=0;\n" 164 "__CPROVER_size_t __CPROVER_malloc_size;\n" 165 "__CPROVER_bool __CPROVER_malloc_is_new_array=0;\n" 166 "const void *__CPROVER_memory_leak=0;\n" 170 "extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];\n" 174 "extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];\n" 176 "extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];\n" 179 "__CPROVER_bool __CPROVER_isnanf(float f);\n" 180 "__CPROVER_bool __CPROVER_isnand(double f);\n" 181 "__CPROVER_bool __CPROVER_isnanld(long double f);\n" 182 "__CPROVER_bool __CPROVER_isfinitef(float f);\n" 183 "__CPROVER_bool __CPROVER_isfinited(double f);\n" 184 "__CPROVER_bool __CPROVER_isfiniteld(long double f);\n" 185 "__CPROVER_bool __CPROVER_isinff(float f);\n" 186 "__CPROVER_bool __CPROVER_isinfd(double f);\n" 187 "__CPROVER_bool __CPROVER_isinfld(long double f);\n" 188 "__CPROVER_bool __CPROVER_isnormalf(float f);\n" 189 "__CPROVER_bool __CPROVER_isnormald(double f);\n" 190 "__CPROVER_bool __CPROVER_isnormalld(long double f);\n" 191 "__CPROVER_bool __CPROVER_signf(float f);\n" 192 "__CPROVER_bool __CPROVER_signd(double f);\n" 193 "__CPROVER_bool __CPROVER_signld(long double f);\n" 194 "double __CPROVER_inf(void);\n" 195 "float __CPROVER_inff(void);\n" 196 "long double __CPROVER_infl(void);\n" 197 "int __CPROVER_thread_local __CPROVER_rounding_mode="+
199 "int __CPROVER_isgreaterf(float f, float g);\n" 200 "int __CPROVER_isgreaterd(double f, double g);\n" 201 "int __CPROVER_isgreaterequalf(float f, float g);\n" 202 "int __CPROVER_isgreaterequald(double f, double g);\n" 203 "int __CPROVER_islessf(float f, float g);\n" 204 "int __CPROVER_islessd(double f, double g);\n" 205 "int __CPROVER_islessequalf(float f, float g);\n" 206 "int __CPROVER_islessequald(double f, double g);\n" 207 "int __CPROVER_islessgreaterf(float f, float g);\n" 208 "int __CPROVER_islessgreaterd(double f, double g);\n" 209 "int __CPROVER_isunorderedf(float f, float g);\n" 210 "int __CPROVER_isunorderedd(double f, double g);\n" 213 "int __CPROVER_abs(int x);\n" 214 "long int __CPROVER_labs(long int x);\n" 215 "long int __CPROVER_llabs(long long int x);\n" 216 "double __CPROVER_fabs(double x);\n" 217 "long double __CPROVER_fabsl(long double x);\n" 218 "float __CPROVER_fabsf(float x);\n" 222 "__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);\n" 225 "void __CPROVER_array_copy(const void *dest, const void *src);\n" 227 "void __CPROVER_array_replace(const void *dest, const void *src);\n" 228 "void __CPROVER_array_set(const void *dest, ...);\n" 231 "void __CPROVER_k_induction_hint(unsigned min, unsigned max, " 232 "unsigned step, unsigned loop_free);\n" 235 "int __CPROVER_scanf(const char *, ...);\n" 238 "struct __CPROVER_pipet {\n" 241 " short next_avail;\n" 242 " short next_unread;\n" 245 "extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];\n" 247 "extern const int __CPROVER_pipe_offset;\n" 248 "unsigned __CPROVER_pipe_count=0;\n" 273 code+=
"typedef double __float128;\n";
311 code+=
"typedef signed __int128 __int128_t;\n" 312 "typedef unsigned __int128 __uint128_t;\n";
318 code+=
"int __noop();\n" 319 "int __assume(int);\n";
339 code+=
"# 1 \"<builtin-architecture-strings>\"\n";
struct configt::ansi_ct ansi_c
const std::string & id2string(const irep_idt &d)
const char gcc_builtin_headers_ia32_3[]
const char gcc_builtin_headers_ubsan[]
static std::string os_to_string(ost)
const char gcc_builtin_headers_alpha[]
const char arm_builtin_headers[]
void ansi_c_internal_additions(std::string &code)
const char cw_builtin_headers[]
const char gcc_builtin_headers_omp[]
const char gcc_builtin_headers_mips[]
static std::string architecture_string(const std::string &value, const char *s)
unsigned long_long_int_width
void ansi_c_architecture_strings(std::string &code)
const char gcc_builtin_headers_generic[]
const char gcc_builtin_headers_tm[]
unsigned memory_operand_size
const char gcc_builtin_headers_mem_string[]
const char gcc_builtin_headers_ia32_4[]
ieee_floatt::rounding_modet rounding_mode
const char clang_builtin_headers[]
const char gcc_builtin_headers_math[]
unsigned long_double_width
const char gcc_builtin_headers_ia32[]
const char gcc_builtin_headers_arm[]
const char gcc_builtin_headers_ia32_2[]
const char gcc_builtin_headers_power[]