CBMC: /home/runner/work/cbmc/cbmc/src/cpp/cpp_internal_additions.cpp Source File

CBMC
Loading...
Searching...
No Matches
cpp_internal_additions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "cpp_internal_additions.h"
10
11#include <ostream>
12
13#include <util/c_types.h>
14#include <util/config.h>
15
16#include <ansi-c/ansi_c_internal_additions.h>
17
18#include <linking/static_lifetime_init.h>
19
20#include <goto-programs/adjust_float_expressions.h>
21
22 std::string c2cpp(const std::string &s)
23{
24 std::string result;
25
26 result.reserve(s.size());
27
28 for(std::size_t i=0; i<s.size(); i++)
29 {
30 char ch=s[i];
31
32 if(ch=='_' && std::string(s, i, 5)=="_Bool")
33 {
34 result.append("bool");
35 i+=4;
36 continue;
37 }
38
39 result+=ch;
40 }
41
42 return result;
43}
44
45 void cpp_internal_additions(std::ostream &out)
46{
47 out << "#line 1 \"<built-in-additions>\"" << '\n';
48
49 // __CPROVER namespace
50 out << "namespace __CPROVER { }" << '\n';
51
52 // types
53 out << "typedef __typeof__(sizeof(int)) __CPROVER::size_t;" << '\n';
54 out << "typedef __CPROVER::size_t " CPROVER_PREFIX "size_t;" << '\n';
55 out << "typedef "
57 << " __CPROVER::ssize_t;" << '\n';
58 out << "typedef __CPROVER::ssize_t " CPROVER_PREFIX "ssize_t;" << '\n';
59
60 // new and delete are in the root namespace!
61 out << "void operator delete(void *);" << '\n';
62 out << "void *operator new(__CPROVER::size_t);" << '\n';
63
64 out << "extern \"C\" {" << '\n';
65
66 // CPROVER extensions
67 out << "const unsigned __CPROVER::constant_infinity_uint;" << '\n';
68 out << "typedef void " CPROVER_PREFIX "integer;" << '\n';
69 out << "typedef void " CPROVER_PREFIX "rational;" << '\n';
70
71 // malloc
72 out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n';
73 out << "const void *" CPROVER_PREFIX "dead_object = 0;" << '\n';
74 out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n';
75 out << "void *" CPROVER_PREFIX "allocate("
76 << CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);" << '\n';
77
78 // auxiliaries for new/delete
79 out << "void *__new(__CPROVER::size_t);" << '\n';
80 out << "void *__new_array(__CPROVER::size_t, __CPROVER::size_t);" << '\n';
81 out << "void *__placement_new(__CPROVER::size_t, void *);" << '\n';
82 out << "void *__placement_new_array("
83 << "__CPROVER::size_t, __CPROVER::size_t, void *);" << '\n';
84 out << "void __delete(void *);" << '\n';
85 out << "void __delete_array(void *);" << '\n';
86
87 // float
88 // TODO: should be thread_local
89 out << "int " << rounding_mode_identifier() << " = "
90 << std::to_string(config.ansi_c.rounding_mode) << ';' << '\n';
91
92 // pipes, write, read, close
93 out << "struct " CPROVER_PREFIX "pipet {\n"
94 << " bool widowed;\n"
95 << " char data[4];\n"
96 << " short next_avail;\n"
97 << " short next_unread;\n"
98 << "};\n";
99
100 // This function needs to be declared, or otherwise can't be called
101 // by the entry-point construction.
102 out << "void " INITIALIZE_FUNCTION "();" << '\n';
103
104 // GCC junk stuff, also for CLANG and ARM
105 if(
109 {
111
112 if(
113 config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
114 config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64" ||
115 config.ansi_c.arch == "powerpc" || config.ansi_c.arch == "ppc64")
116 {
117 // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
118 // For clang, __float128 is a keyword.
119 // For gcc, this is a typedef and not a keyword.
120 // C++ doesn't have _Float128.
122 out << "typedef " CPROVER_PREFIX "Float128 __float128;" << '\n';
123 }
124 else if(config.ansi_c.arch == "hppa")
125 {
126 // https://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
127 // For clang, __float128 is a keyword.
128 // For gcc, this is a typedef and not a keyword.
129 // C++ doesn't have _Float128.
131 out << "typedef long double __float128;" << '\n';
132 }
133 else if(config.ansi_c.arch == "ppc64le")
134 {
135 // https://patchwork.ozlabs.org/patch/792295/
137 out << "typedef " CPROVER_PREFIX "Float128 __ieee128;\n";
138 }
139
140 if(
141 config.ansi_c.arch == "i386" || config.ansi_c.arch == "x86_64" ||
142 config.ansi_c.arch == "x32" || config.ansi_c.arch == "ia64")
143 {
144 // clang doesn't do __float80
145 // Note that __float80 is a typedef, and not a keyword,
146 // and that C++ doesn't have _Float64x.
148 out << "typedef " CPROVER_PREFIX "Float80 __float80;" << '\n';
149 }
150
151 // On 64-bit systems, gcc has typedefs
152 // __int128_t und __uint128_t -- but not on 32 bit!
153 if(config.ansi_c.long_int_width >= 64)
154 {
155 out << "typedef signed __int128 __int128_t;" << '\n';
156 out << "typedef unsigned __int128 __uint128_t;" << '\n';
157 }
158
159 if(
160 config.ansi_c.arch == "arm64" &&
162 {
163 out << "typedef struct __va_list {";
164 out << "void *__stack;";
165 out << "void *__gr_top;";
166 out << "void *__vr_top;";
167 out << "int __gr_offs;";
168 out << "int __vr_offs;";
169 out << " } __builtin_va_list;" << '\n';
170 }
171 else
172 {
173 out << "typedef void ** __builtin_va_list;" << '\n';
174 }
175 }
176
177 // this is Visual C/C++ only
179 {
180 out << "int __noop(...);" << '\n';
181 out << "int __assume(int);" << '\n';
182 }
183
184 // ARM stuff
187
188 // CW stuff
191
192 // string symbols to identify the architecture we have compiled for
193 std::string architecture_strings;
196
197 out << '}' << '\n'; // end extern "C"
198
199 // Microsoft stuff
201 {
202 // type_info infrastructure -- the standard wants this to be in the
203 // std:: namespace, but MS has it in the root namespace
204 out << "class type_info;" << '\n';
205
206 // this is the return type of __uuidof(...),
207 // in the root namespace
208 out << "struct _GUID;" << '\n';
209
210 // MS ATL-related stuff
211 out << "namespace ATL; " << '\n';
212 out << "void ATL::AtlThrowImpl(long);" << '\n';
213 out << "void __stdcall ATL::AtlThrowLastWin32();" << '\n';
214 }
215
216 out << std::flush;
217}
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
const char gcc_builtin_headers_types[]
const char cw_builtin_headers[]
const char arm_builtin_headers[]
void ansi_c_architecture_strings(std::string &code)
configt config
Definition config.cpp:25
std::string c_type_as_string(const irep_idt &c_type)
Definition c_types.cpp:251
signedbv_typet signed_size_type()
Definition c_types.cpp:66
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
struct configt::ansi_ct ansi_c
std::string c2cpp(const std::string &s)
void cpp_internal_additions(std::ostream &out)
#define CPROVER_PREFIX
#define INITIALIZE_FUNCTION
@ OS_WIN
@ OS_MACOS
@ GCC
@ ARM
@ VISUAL_STUDIO
@ CLANG
@ CODEWARRIOR

AltStyle によって変換されたページ (->オリジナル) /