20 std::string
c2cpp(
const std::string &s)
24 result.reserve(s.size());
26 for(std::size_t i=0; i<s.size(); i++)
30 if(ch==
'_' && std::string(s, i, 5)==
"_Bool")
32 result.append(
"bool");
45 out <<
"# 1 \"<built-in-additions>\"" <<
'\n';
48 out <<
"namespace __CPROVER { }" <<
'\n';
51 out <<
"typedef __typeof__(sizeof(int)) __CPROVER::size_t;" <<
'\n';
52 out <<
"typedef __CPROVER::size_t __CPROVER_size_t;" <<
'\n';
55 <<
" __CPROVER::ssize_t;" <<
'\n';
56 out <<
"typedef __CPROVER::ssize_t __CPROVER_ssize_t;" <<
'\n';
59 out <<
"void operator delete(void *);" <<
'\n';
60 out <<
"void *operator new(__CPROVER::size_t);" <<
'\n';
62 out <<
"extern \"C\" {" <<
'\n';
65 out <<
"const unsigned __CPROVER::constant_infinity_uint;" <<
'\n';
66 out <<
"typedef void __CPROVER_integer;" <<
'\n';
67 out <<
"typedef void __CPROVER_rational;" <<
'\n';
70 out <<
"__CPROVER_bool " 71 <<
"__CPROVER_threads_exited[__CPROVER::constant_infinity_uint];" <<
'\n';
72 out <<
"unsigned long __CPROVER_next_thread_id = 0;" <<
'\n';
73 out <<
"extern unsigned char " 74 <<
"__CPROVER_memory[__CPROVER::constant_infinity_uint];" <<
'\n';
77 out <<
"const void *__CPROVER_deallocated = 0;" <<
'\n';
78 out <<
"const void *__CPROVER_dead_object = 0;" <<
'\n';
79 out <<
"const void *__CPROVER_malloc_object = 0;" <<
'\n';
80 out <<
"__CPROVER::size_t __CPROVER_malloc_size;" <<
'\n';
81 out <<
"__CPROVER_bool __CPROVER_malloc_is_new_array = 0;" <<
'\n';
82 out <<
"const void *__CPROVER_memory_leak = 0;" <<
'\n';
83 out <<
"void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);" 87 out <<
"void *__new(__CPROVER::size_t);" <<
'\n';
88 out <<
"void *__new_array(__CPROVER::size_t, __CPROVER::size_t);" <<
'\n';
89 out <<
"void *__placement_new(__CPROVER::size_t, void *);" <<
'\n';
90 out <<
"void *__placement_new_array(" 91 <<
"__CPROVER::size_t, __CPROVER::size_t, void *);" <<
'\n';
92 out <<
"void __delete(void *);" <<
'\n';
93 out <<
"void __delete_array(void *);" <<
'\n';
97 out <<
"int __CPROVER_rounding_mode = " 101 out <<
"struct __CPROVER_pipet {\n" 102 <<
" bool widowed;\n" 103 <<
" char data[4];\n" 104 <<
" short next_avail;\n" 105 <<
" short next_unread;\n" 107 out <<
"extern struct __CPROVER_pipet " 108 <<
"__CPROVER_pipes[__CPROVER::constant_infinity_uint];" <<
'\n';
110 out <<
"extern const int __CPROVER_pipe_offset;" <<
'\n';
111 out <<
"unsigned __CPROVER_pipe_count=0;" <<
'\n';
136 out <<
"typedef __CPROVER_Float128 __float128;" <<
'\n';
145 out <<
"typedef long double __float128;" <<
'\n';
156 out <<
"typedef __CPROVER_Float80 __float80;" <<
'\n';
163 out <<
"typedef signed __int128 __int128_t;" <<
'\n';
164 out <<
"typedef unsigned __int128 __uint128_t;" <<
'\n';
171 out <<
"int __noop(...);" <<
'\n';
172 out <<
"int __assume(int);" <<
'\n';
184 std::string architecture_strings;
186 out <<
c2cpp(architecture_strings);
195 out <<
"class type_info;" <<
'\n';
199 out <<
"struct _GUID;" <<
'\n';
202 out <<
"namespace ATL; " <<
'\n';
203 out <<
"void ATL::AtlThrowImpl(long);" <<
'\n';
204 out <<
"void __stdcall ATL::AtlThrowLastWin32();" <<
'\n';
struct configt::ansi_ct ansi_c
const char gcc_builtin_headers_types[]
signedbv_typet signed_size_type()
const char arm_builtin_headers[]
const char cw_builtin_headers[]
void cpp_internal_additions(std::ostream &out)
std::string c2cpp(const std::string &s)
#define INITIALIZE_FUNCTION
void ansi_c_architecture_strings(std::string &code)
std::string c_type_as_string(const irep_idt &c_type)
ieee_floatt::rounding_modet rounding_mode
std::string to_string(const string_constraintt &expr)
Used for debug printing.
std::size_t long_int_width