cprover
cpp_internal_additions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
10 
11 #include <ostream>
12 
13 #include <util/config.h>
14 
16 
17 std::string c2cpp(const std::string &s)
18 {
19  std::string result;
20 
21  result.reserve(s.size());
22 
23  for(unsigned i=0; i<s.size(); i++)
24  {
25  char ch=s[i];
26 
27  if(ch=='_' && std::string(s, i, 5)=="_Bool")
28  {
29  result.append("bool");
30  i+=4;
31  continue;
32  }
33 
34  result+=ch;
35  }
36 
37  return result;
38 }
39 
40 void cpp_internal_additions(std::ostream &out)
41 {
42  out << "# 1 \"<built-in>\"" << '\n';
43 
44  // new and delete are in the root namespace!
45  out << "void operator delete(void *);" << '\n';
46  out << "void *operator new(__typeof__(sizeof(int)));" << '\n';
47 
48  // auxiliaries for new/delete
49  out << "extern \"C\" void *__new(__typeof__(sizeof(int)));" << '\n';
50  // NOLINTNEXTLINE(whitespace/line_length)
51  out << "extern \"C\" void *__new_array(__typeof__(sizeof(int)), __typeof__(sizeof(int)));" << '\n';
52  // NOLINTNEXTLINE(whitespace/line_length)
53  out << "extern \"C\" void *__placement_new(__typeof__(sizeof(int)), void *);" << '\n';
54  // NOLINTNEXTLINE(whitespace/line_length)
55  out << "extern \"C\" void *__placement_new_array(__typeof__(sizeof(int)), __typeof__(sizeof(int)), void *);" << '\n';
56  out << "extern \"C\" void __delete(void *);" << '\n';
57  out << "extern \"C\" void __delete_array(void *);" << '\n';
58  out << "extern \"C\" bool __CPROVER_malloc_is_new_array=0;" << '\n';
59 
60  // __CPROVER namespace
61  out << "namespace __CPROVER { }" << '\n';
62 
63  // types
64  out << "typedef __typeof__(sizeof(int)) __CPROVER::size_t;" << '\n';
65  out << "typedef __typeof__(sizeof(int)) __CPROVER_size_t;" << '\n';
66 
67  // assume/assert
68  out << "extern \"C\" void assert(bool assertion);" << '\n';
69  out << "extern \"C\" void __CPROVER_assume(bool assumption);" << '\n';
70  out << "extern \"C\" void __CPROVER_assert("
71  "bool assertion, const char *description);" << '\n';
72  out << "extern \"C\" void __CPROVER::assume(bool assumption);" << '\n';
73  out << "extern \"C\" void __CPROVER::assert("
74  "bool assertion, const char *description);" << '\n';
75 
76  // CPROVER extensions
77  out << "extern \"C\" const unsigned __CPROVER::constant_infinity_uint;\n";
78  out << "extern \"C\" void __CPROVER_initialize();" << '\n';
79  out << "extern \"C\" void __CPROVER::input(const char *id, ...);" << '\n';
80  out << "extern \"C\" void __CPROVER::output(const char *id, ...);" << '\n';
81  out << "extern \"C\" void __CPROVER::cover(bool condition);" << '\n';
82  out << "extern \"C\" void __CPROVER::atomic_begin();" << '\n';
83  out << "extern \"C\" void __CPROVER::atomic_end();" << '\n';
84 
85  // pointers
86  out << "extern \"C\" unsigned __CPROVER_POINTER_OBJECT(const void *p);\n";
87  out << "extern \"C\" signed __CPROVER_POINTER_OFFSET(const void *p);" << '\n';
88  out << "extern \"C\" bool __CPROVER_DYNAMIC_OBJECT(const void *p);" << '\n';
89  // NOLINTNEXTLINE(whitespace/line_length)
90  out << "extern \"C\" extern unsigned char __CPROVER_memory[__CPROVER::constant_infinity_uint];" << '\n';
91  out << "extern \"C\" const void *__CPROVER_dead_object=0;" << '\n';
92 
93  // malloc
94  out << "extern \"C\" void *__CPROVER_malloc(__CPROVER::size_t size);" << '\n';
95  out << "extern \"C\" const void *__CPROVER_deallocated=0;" << '\n';
96  out << "extern \"C\" const void *__CPROVER_malloc_object=0;" << '\n';
97  out << "extern \"C\" __CPROVER::size_t __CPROVER_malloc_size;" << '\n';
98 
99  // float
100  out << "extern \"C\" int __CPROVER_rounding_mode;" << '\n';
101 
102  // arrays
103  // NOLINTNEXTLINE(whitespace/line_length)
104  out << "bool __CPROVER::array_equal(const void array1[], const void array2[]);" << '\n';
105  out << "void __CPROVER::array_copy(const void dest[], const void src[]);\n";
106  out << "void __CPROVER::array_set(const void dest[], ...);" << '\n';
107 
108  // GCC stuff, but also for ARM
112  {
113  out << "extern \"C\" {" << '\n';
121 
123  out << "typedef double __float128;\n"; // clang doesn't do __float128
124 
129  out << "}" << '\n';
130  }
131 
132  // extensions for Visual C/C++
134  out << "extern \"C\" int __noop(...);\n";
135 
136  // string symbols to identify the architecture we have compiled for
137  std::string architecture_strings;
138  ansi_c_architecture_strings(architecture_strings);
139 
140  out << "extern \"C\" {" << '\n';
141  out << architecture_strings;
142  out << "}" << '\n';
143 
144  // Microsoft stuff
146  {
147  // type_info infrastructure -- the standard wants this to be in the
148  // std:: namespace, but MS has it in the root namespace
149  out << "class type_info;" << '\n';
150 
151  // this is the return type of __uuidof(...),
152  // in the root namespace
153  out << "struct _GUID;" << '\n';
154 
155  // MS ATL-related stuff
156  out << "namespace ATL; " << '\n';
157  out << "void ATL::AtlThrowImpl(long);" << '\n';
158  out << "void __stdcall ATL::AtlThrowLastWin32();" << '\n';
159  }
160 
161  out << std::flush;
162 }
struct configt::ansi_ct ansi_c
const char gcc_builtin_headers_ia32_3[]
const char gcc_builtin_headers_ubsan[]
configt config
Definition: config.cpp:21
const char gcc_builtin_headers_omp[]
void cpp_internal_additions(std::ostream &out)
flavourt mode
Definition: config.h:105
std::string c2cpp(const std::string &s)
void ansi_c_architecture_strings(std::string &code)
const char gcc_builtin_headers_generic[]
const char gcc_builtin_headers_tm[]
const char gcc_builtin_headers_mem_string[]
const char gcc_builtin_headers_ia32_4[]
const char clang_builtin_headers[]
const char gcc_builtin_headers_math[]
const char gcc_builtin_headers_ia32[]
const char gcc_builtin_headers_ia32_2[]