diff --git a/src/ansi-c/CMakeLists.txt b/src/ansi-c/CMakeLists.txt index fea313b21b8..be4d003342e 100644 --- a/src/ansi-c/CMakeLists.txt +++ b/src/ansi-c/CMakeLists.txt @@ -72,6 +72,7 @@ make_inc(gcc_builtin_headers_mips) make_inc(gcc_builtin_headers_omp) make_inc(gcc_builtin_headers_power) make_inc(gcc_builtin_headers_tm) +make_inc(gcc_builtin_headers_types) make_inc(gcc_builtin_headers_ubsan) set(extra_dependencies @@ -92,6 +93,7 @@ set(extra_dependencies ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_omp.inc ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_power.inc ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_tm.inc + ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_types.inc ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ubsan.inc ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp ) diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index 559bff9603d..97519b2a4df 100644 --- a/src/ansi-c/Makefile +++ b/src/ansi-c/Makefile @@ -10,6 +10,7 @@ SRC = anonymous_member.cpp \ ansi_c_scope.cpp \ ansi_c_typecheck.cpp \ ansi_c_y.tab.cpp \ + builtin_factory.cpp \ c_misc.cpp \ c_nondet_symbol_factory.cpp \ c_preprocess.cpp \ @@ -43,20 +44,32 @@ INCLUDES= -I .. include ../config.inc include ../common +BUILTIN_FILES = \ + arm_builtin_headers.inc \ + clang_builtin_headers.inc \ + cw_builtin_headers.inc \ + gcc_builtin_headers_alpha.inc \ + gcc_builtin_headers_arm.inc \ + gcc_builtin_headers_generic.inc \ + gcc_builtin_headers_ia32-2.inc \ + gcc_builtin_headers_ia32-3.inc \ + gcc_builtin_headers_ia32-4.inc \ + gcc_builtin_headers_ia32.inc \ + gcc_builtin_headers_math.inc \ + gcc_builtin_headers_mem_string.inc \ + gcc_builtin_headers_mips.inc \ + gcc_builtin_headers_omp.inc \ + gcc_builtin_headers_power.inc \ + gcc_builtin_headers_tm.inc \ + gcc_builtin_headers_types.inc \ + gcc_builtin_headers_ubsan.inc + CLEANFILES = ansi-c$(LIBEXT) \ ansi_c_y.tab.h ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.cpp.output \ ansi_c_y.output \ library/converter$(EXEEXT) cprover_library.inc \ file_converter$(EXEEXT) library_check \ - gcc_builtin_headers_generic.inc gcc_builtin_headers_ia32.inc \ - arm_builtin_headers.inc cw_builtin_headers.inc \ - gcc_builtin_headers_arm.inc gcc_builtin_headers_alpha.inc \ - gcc_builtin_headers_mips.inc gcc_builtin_headers_power.inc \ - clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \ - gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \ - gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \ - gcc_builtin_headers_mem_string.inc \ - gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc + $(BUILTIN_FILES) all: ansi-c$(LIBEXT) @@ -102,34 +115,12 @@ cprover_library.inc: library/converter$(EXEEXT) library/*.c cprover_library.cpp: cprover_library.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_generic.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-2.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-3.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ia32-4.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_alpha.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_arm.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_math.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mem_string.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_mips.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_omp.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_power.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_tm.inc -ansi_c_internal_additions$(OBJEXT): gcc_builtin_headers_ubsan.inc -ansi_c_internal_additions$(OBJEXT): arm_builtin_headers.inc -ansi_c_internal_additions$(OBJEXT): cw_builtin_headers.inc -ansi_c_internal_additions$(OBJEXT): clang_builtin_headers.inc - -generated_files: cprover_library.inc gcc_builtin_headers_generic.inc \ - gcc_builtin_headers_ia32.inc gcc_builtin_headers_alpha.inc \ - gcc_builtin_headers_arm.inc gcc_builtin_headers_mips.inc \ - gcc_builtin_headers_power.inc arm_builtin_headers.inc \ - cw_builtin_headers.inc ansi_c_y.tab.cpp ansi_c_lex.yy.cpp \ - ansi_c_y.tab.h clang_builtin_headers.inc gcc_builtin_headers_ia32-2.inc \ - gcc_builtin_headers_math.inc gcc_builtin_headers_omp.inc \ - gcc_builtin_headers_tm.inc gcc_builtin_headers_ubsan.inc \ - gcc_builtin_headers_mem_string.inc \ - gcc_builtin_headers_ia32-3.inc gcc_builtin_headers_ia32-4.inc +ansi_c_internal_additions$(OBJEXT): $(BUILTIN_FILES) + +generated_files: \ + ansi_c_y.tab.cpp ansi_c_lex.yy.cpp ansi_c_y.tab.h \ + cprover_library.inc \ + $(BUILTIN_FILES) ############################################################################### diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 401ff940ce6..abcf362a943 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -10,6 +10,11 @@ Author: Daniel Kroening, kroening@kroening.com #include +const char gcc_builtin_headers_types[]= +"# 1 \"gcc_builtin_headers_types.h\"\n" +#include "gcc_builtin_headers_types.inc" +; // NOLINT(whitespace/semicolon) + const char gcc_builtin_headers_generic[]= "# 1 \"gcc_builtin_headers_generic.h\"\n" #include "gcc_builtin_headers_generic.inc" @@ -89,6 +94,10 @@ const char clang_builtin_headers[]= #include "clang_builtin_headers.inc" ; // NOLINT(whitespace/semicolon) +const char windows_builtin_headers[]= + "int __noop();\n" + "int __assume(int);\n"; + static std::string architecture_string(const std::string &value, const char *s) { return std::string("const char *__CPROVER_architecture_")+ @@ -257,13 +266,7 @@ void ansi_c_internal_additions(std::string &code) config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE || config.ansi_c.mode==configt::ansi_ct::flavourt::ARM) { - code+=gcc_builtin_headers_generic; - code+=gcc_builtin_headers_math; - code+=gcc_builtin_headers_mem_string; - code+=gcc_builtin_headers_omp; - code+=gcc_builtin_headers_tm; - code+=gcc_builtin_headers_ubsan; - code+=clang_builtin_headers; + code+=gcc_builtin_headers_types; // there are many more, e.g., look at // https://developer.apple.com/library/mac/#documentation/developertools/gcc-4.0.1/gcc/Target-Builtins.html @@ -274,37 +277,6 @@ void ansi_c_internal_additions(std::string &code) { if(config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE) code+="typedef double __float128;\n"; // clang doesn't do __float128 - - code+=gcc_builtin_headers_ia32; - code+=gcc_builtin_headers_ia32_2; - code+=gcc_builtin_headers_ia32_3; - code+=gcc_builtin_headers_ia32_4; - } - else if(config.ansi_c.arch=="arm64" || - config.ansi_c.arch=="armel" || - config.ansi_c.arch=="armhf" || - config.ansi_c.arch=="arm") - { - code+=gcc_builtin_headers_arm; - } - else if(config.ansi_c.arch=="alpha") - { - code+=gcc_builtin_headers_alpha; - } - else if(config.ansi_c.arch=="mips64el" || - config.ansi_c.arch=="mipsn32el" || - config.ansi_c.arch=="mipsel" || - config.ansi_c.arch=="mips64" || - config.ansi_c.arch=="mipsn32" || - config.ansi_c.arch=="mips") - { - code+=gcc_builtin_headers_mips; - } - else if(config.ansi_c.arch=="powerpc" || - config.ansi_c.arch=="ppc64" || - config.ansi_c.arch=="ppc64le") - { - code+=gcc_builtin_headers_power; } // On 64-bit systems, gcc has typedefs diff --git a/src/ansi-c/ansi_c_internal_additions.h b/src/ansi-c/ansi_c_internal_additions.h index a0977a35331..10e7c8e144d 100644 --- a/src/ansi-c/ansi_c_internal_additions.h +++ b/src/ansi-c/ansi_c_internal_additions.h @@ -15,17 +15,24 @@ Author: Daniel Kroening, kroening@kroening.com void ansi_c_internal_additions(std::string &code); void ansi_c_architecture_strings(std::string &code); +extern const char clang_builtin_headers[]; +extern const char gcc_builtin_headers_types[]; extern const char gcc_builtin_headers_generic[]; extern const char gcc_builtin_headers_math[]; extern const char gcc_builtin_headers_mem_string[]; extern const char gcc_builtin_headers_omp[]; extern const char gcc_builtin_headers_tm[]; extern const char gcc_builtin_headers_ubsan[]; -extern const char clang_builtin_headers[]; extern const char gcc_builtin_headers_ia32[]; extern const char gcc_builtin_headers_ia32_2[]; extern const char gcc_builtin_headers_ia32_3[]; extern const char gcc_builtin_headers_ia32_4[]; +extern const char gcc_builtin_headers_alpha[]; +extern const char gcc_builtin_headers_arm[]; +extern const char gcc_builtin_headers_mips[]; +extern const char gcc_builtin_headers_power[]; extern const char arm_builtin_headers[]; +extern const char cw_builtin_headers[]; +extern const char windows_builtin_headers[]; #endif // CPROVER_ANSI_C_ANSI_C_INTERNAL_ADDITIONS_H diff --git a/src/ansi-c/builtin_factory.cpp b/src/ansi-c/builtin_factory.cpp new file mode 100644 index 00000000000..cd839a46223 --- /dev/null +++ b/src/ansi-c/builtin_factory.cpp @@ -0,0 +1,202 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "builtin_factory.h" +#include "ansi_c_internal_additions.h" + +#include "ansi_c_parser.h" +#include "ansi_c_typecheck.h" + +#include +#include + +#include +#include + +static bool find_pattern( + const std::string &pattern, + const char *header_file, + std::ostream &out) +{ + std::istringstream hdr(header_file); + std::string line; + while(std::getline(hdr, line)) + { + line = strip_string(line); + if(has_prefix(line, "//") || line.find(pattern) == std::string::npos) + continue; + + out << line; + return true; + } + + return false; +} + +static bool convert( + const irep_idt &identifier, + const std::ostringstream &s, + symbol_tablet &symbol_table, + message_handlert &message_handler) +{ + std::istringstream in(s.str()); + + ansi_c_parser.clear(); + ansi_c_parser.set_file(ID_built_in); + ansi_c_parser.in=∈ + ansi_c_parser.set_message_handler(message_handler); + ansi_c_parser.for_has_scope=config.ansi_c.for_has_scope; + ansi_c_parser.cpp98=false; // it's not C++ + ansi_c_parser.cpp11=false; // it's not C++ + ansi_c_parser.mode=config.ansi_c.mode; + + ansi_c_scanner_init(); + + if(ansi_c_parser.parse()) + return true; + + symbol_tablet new_symbol_table; + + // this is recursive -- builtin_factory is called + // from the typechecker + if(ansi_c_typecheck( + ansi_c_parser.parse_tree, + new_symbol_table, + "", // module + message_handler)) + { + return true; + } + + // we should now have a new symbol + symbol_tablet::symbolst::const_iterator s_it= + new_symbol_table.symbols.find(identifier); + + if(s_it==new_symbol_table.symbols.end()) + { + messaget message(message_handler); + message.error() << "failed to produce built-in symbol `" + << identifier << '\'' << messaget::eom; + return true; + } + + // copy the new symbol + symbol_table.add(s_it->second); + + return false; +} + +//! Check whether given identifier is a compiler built-in. +//! If so, add declaration to symbol table. +//! \return 'true' on error +bool builtin_factory( + const irep_idt &identifier, + symbol_tablet &symbol_table, + message_handlert &mh) +{ + // we search for "space" "identifier" "(" + const std::string pattern=' '+id2string(identifier)+'('; + + std::ostringstream s; + + std::string code; + ansi_c_internal_additions(code); + s << code; + + // this is Visual C/C++ only + if(config.ansi_c.os==configt::ansi_ct::ost::OS_WIN) + { + if(find_pattern(pattern, windows_builtin_headers, s)) + return convert(identifier, s, symbol_table, mh); + } + + // ARM stuff + if(config.ansi_c.mode==configt::ansi_ct::flavourt::ARM) + { + if(find_pattern(pattern, arm_builtin_headers, s)) + return convert(identifier, s, symbol_table, mh); + } + + // CW stuff + if(config.ansi_c.mode==configt::ansi_ct::flavourt::CODEWARRIOR) + { + if(find_pattern(pattern, cw_builtin_headers, s)) + return convert(identifier, s, symbol_table, mh); + } + + // GCC junk stuff, also for CLANG and ARM + if(config.ansi_c.mode==configt::ansi_ct::flavourt::GCC || + config.ansi_c.mode==configt::ansi_ct::flavourt::APPLE || + config.ansi_c.mode==configt::ansi_ct::flavourt::ARM) + { + if(find_pattern(pattern, gcc_builtin_headers_generic, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_math, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_mem_string, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_omp, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_tm, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_ubsan, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, clang_builtin_headers, s)) + return convert(identifier, s, symbol_table, mh); + + if(config.ansi_c.arch=="i386" || + config.ansi_c.arch=="x86_64" || + config.ansi_c.arch=="x32") + { + if(find_pattern(pattern, gcc_builtin_headers_ia32, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_ia32_2, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_ia32_3, s)) + return convert(identifier, s, symbol_table, mh); + + if(find_pattern(pattern, gcc_builtin_headers_ia32_4, s)) + return convert(identifier, s, symbol_table, mh); + } + else if(config.ansi_c.arch=="arm64" || + config.ansi_c.arch=="armel" || + config.ansi_c.arch=="armhf" || + config.ansi_c.arch=="arm") + { + if(find_pattern(pattern, gcc_builtin_headers_arm, s)) + return convert(identifier, s, symbol_table, mh); + } + else if(config.ansi_c.arch=="mips64el" || + config.ansi_c.arch=="mipsn32el" || + config.ansi_c.arch=="mipsel" || + config.ansi_c.arch=="mips64" || + config.ansi_c.arch=="mipsn32" || + config.ansi_c.arch=="mips") + { + if(find_pattern(pattern, gcc_builtin_headers_mips, s)) + return convert(identifier, s, symbol_table, mh); + } + else if(config.ansi_c.arch=="powerpc" || + config.ansi_c.arch=="ppc64" || + config.ansi_c.arch=="ppc64le") + { + if(find_pattern(pattern, gcc_builtin_headers_power, s)) + return convert(identifier, s, symbol_table, mh); + } + } + + return true; +} diff --git a/src/ansi-c/builtin_factory.h b/src/ansi-c/builtin_factory.h new file mode 100644 index 00000000000..9fffb891c26 --- /dev/null +++ b/src/ansi-c/builtin_factory.h @@ -0,0 +1,21 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_ANSI_C_BUILTIN_FACTORY_H +#define CPROVER_ANSI_C_BUILTIN_FACTORY_H + +#include +#include + +//! \return 'true' in case of error +bool builtin_factory( + const irep_idt &identifier, + symbol_tablet &, + message_handlert &); + +#endif // CPROVER_ANSI_C_BUILTIN_FACTORY_H diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 6c7b3ddbcf5..be300c00258 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "builtin_factory.h" #include "c_typecast.h" #include "c_qualifiers.h" #include "anonymous_member.h" @@ -1913,35 +1914,45 @@ void c_typecheck_baset::typecheck_side_effect_function_call( if(symbol_table.symbols.find(identifier)==symbol_table.symbols.end()) { - // This is an undeclared function. Let's just add it. - // We do a bit of return-type guessing, but just a bit. - typet return_type=signed_int_type(); - - // The following isn't really right and sound, but there - // are too many idiots out there who use malloc and the like - // without the right header file. - if(identifier=="malloc" || - identifier=="realloc" || - identifier=="reallocf" || - identifier=="valloc") - return_type=pointer_type(void_type()); // void * - - symbolt new_symbol; - - new_symbol.name=identifier; - new_symbol.base_name=identifier; - new_symbol.location=expr.source_location(); - new_symbol.type=code_typet(); - new_symbol.type.set(ID_C_incomplete, true); - new_symbol.type.add(ID_return_type)=return_type; - - // TODO: should also guess some argument types - - symbolt *symbol_ptr; - move_symbol(new_symbol, symbol_ptr); - - warning().source_location=f_op.find_source_location(); - warning() << "function `" << identifier << "' is not declared" << eom; + // This is an undeclared function. + // Is this a builtin? + if(!builtin_factory(identifier, symbol_table, get_message_handler())) + { + // yes, it's a builtin + } + else + { + // This is an undeclared function that's not a builtin. + // Let's just add it. + // We do a bit of return-type guessing, but just a bit. + typet return_type=signed_int_type(); + + // The following isn't really right and sound, but there + // are too many idiots out there who use malloc and the like + // without the right header file. + if(identifier=="malloc" || + identifier=="realloc" || + identifier=="reallocf" || + identifier=="valloc") + return_type=pointer_type(void_type()); // void * + + symbolt new_symbol; + + new_symbol.name=identifier; + new_symbol.base_name=identifier; + new_symbol.location=expr.source_location(); + new_symbol.type=code_typet(); + new_symbol.type.set(ID_C_incomplete, true); + new_symbol.type.add(ID_return_type)=return_type; + + // TODO: should also guess some argument types + + symbolt *symbol_ptr; + move_symbol(new_symbol, symbol_ptr); + + warning().source_location=f_op.find_source_location(); + warning() << "function `" << identifier << "' is not declared" << eom; + } } } diff --git a/src/ansi-c/clang_builtin_headers.h b/src/ansi-c/clang_builtin_headers.h index 742cba71dbf..2b4b269ca68 100644 --- a/src/ansi-c/clang_builtin_headers.h +++ b/src/ansi-c/clang_builtin_headers.h @@ -1,5 +1,3 @@ -typedef float __gcc_v4sf __attribute__ ((__vector_size__ (16))); - __gcc_v4sf __builtin_shufflevector(__gcc_v4sf, __gcc_v4sf, ...); int __builtin_flt_rounds(void); diff --git a/src/ansi-c/gcc_builtin_headers_generic.h b/src/ansi-c/gcc_builtin_headers_generic.h index 17d997b8deb..908c8f61e3b 100644 --- a/src/ansi-c/gcc_builtin_headers_generic.h +++ b/src/ansi-c/gcc_builtin_headers_generic.h @@ -1,6 +1,3 @@ -typedef void ** __builtin_va_list; -typedef void ** __builtin_ms_va_list; - // stdarg void* __builtin_apply_args(); void __builtin_ms_va_end(void *ap); @@ -105,35 +102,3 @@ void __builtin_return(void*); void* __builtin_saveregs(); int __builtin_setjmp(void*); void __builtin_update_setjmp_buf(void*); - - -typedef int __gcc_m64 __attribute__ ((__vector_size__ (8), __may_alias__)); - -typedef char __gcc_v8qi __attribute__ ((__vector_size__ (8))); -typedef char __gcc_v16qi __attribute__ ((__vector_size__ (16))); -typedef char __gcc_v32qi __attribute__ ((__vector_size__ (32))); -typedef char __gcc_v64qi __attribute__ ((__vector_size__ (64))); -typedef int __gcc_v2si __attribute__ ((__vector_size__ (8))); -typedef int __gcc_v4si __attribute__ ((__vector_size__ (16))); -typedef int __gcc_v8si __attribute__ ((__vector_size__ (32))); -typedef int __gcc_v16si __attribute__ ((__vector_size__ (64))); -typedef short __gcc_v4hi __attribute__ ((__vector_size__ (8))); -typedef short __gcc_v8hi __attribute__ ((__vector_size__ (16))); -typedef short __gcc_v16hi __attribute__ ((__vector_size__ (32))); -typedef short __gcc_v32hi __attribute__ ((__vector_size__ (64))); -typedef float __gcc_v2sf __attribute__ ((__vector_size__ (8))); -typedef float __gcc_v4sf __attribute__ ((__vector_size__ (16))); -typedef float __gcc_v8sf __attribute__ ((__vector_size__ (32))); -typedef float __gcc_v16sf __attribute__ ((__vector_size__ (64))); -typedef double __gcc_v2df __attribute__ ((__vector_size__ (16))); -typedef double __gcc_v4df __attribute__ ((__vector_size__ (32))); -typedef double __gcc_v8df __attribute__ ((__vector_size__ (64))); -typedef long long __gcc_v1di __attribute__ ((__vector_size__ (8))); -typedef long long __gcc_v2di __attribute__ ((__vector_size__ (16))); -typedef long long __gcc_v4di __attribute__ ((__vector_size__ (32))); -typedef long long __gcc_v8di __attribute__ ((__vector_size__ (64))); -typedef unsigned long long __gcc_di; - -enum __gcc_atomic_memmodels { - __ATOMIC_RELAXED, __ATOMIC_CONSUME, __ATOMIC_ACQUIRE, __ATOMIC_RELEASE, __ATOMIC_ACQ_REL, __ATOMIC_SEQ_CST -}; diff --git a/src/ansi-c/gcc_builtin_headers_types.h b/src/ansi-c/gcc_builtin_headers_types.h new file mode 100644 index 00000000000..6278d277440 --- /dev/null +++ b/src/ansi-c/gcc_builtin_headers_types.h @@ -0,0 +1,33 @@ +typedef void ** __builtin_va_list; +typedef void ** __builtin_ms_va_list; + +typedef int __gcc_m64 __attribute__ ((__vector_size__ (8), __may_alias__)); + +typedef char __gcc_v8qi __attribute__ ((__vector_size__ (8))); +typedef char __gcc_v16qi __attribute__ ((__vector_size__ (16))); +typedef char __gcc_v32qi __attribute__ ((__vector_size__ (32))); +typedef char __gcc_v64qi __attribute__ ((__vector_size__ (64))); +typedef int __gcc_v2si __attribute__ ((__vector_size__ (8))); +typedef int __gcc_v4si __attribute__ ((__vector_size__ (16))); +typedef int __gcc_v8si __attribute__ ((__vector_size__ (32))); +typedef int __gcc_v16si __attribute__ ((__vector_size__ (64))); +typedef short __gcc_v4hi __attribute__ ((__vector_size__ (8))); +typedef short __gcc_v8hi __attribute__ ((__vector_size__ (16))); +typedef short __gcc_v16hi __attribute__ ((__vector_size__ (32))); +typedef short __gcc_v32hi __attribute__ ((__vector_size__ (64))); +typedef float __gcc_v2sf __attribute__ ((__vector_size__ (8))); +typedef float __gcc_v4sf __attribute__ ((__vector_size__ (16))); +typedef float __gcc_v8sf __attribute__ ((__vector_size__ (32))); +typedef float __gcc_v16sf __attribute__ ((__vector_size__ (64))); +typedef double __gcc_v2df __attribute__ ((__vector_size__ (16))); +typedef double __gcc_v4df __attribute__ ((__vector_size__ (32))); +typedef double __gcc_v8df __attribute__ ((__vector_size__ (64))); +typedef long long __gcc_v1di __attribute__ ((__vector_size__ (8))); +typedef long long __gcc_v2di __attribute__ ((__vector_size__ (16))); +typedef long long __gcc_v4di __attribute__ ((__vector_size__ (32))); +typedef long long __gcc_v8di __attribute__ ((__vector_size__ (64))); +typedef unsigned long long __gcc_di; + +enum __gcc_atomic_memmodels { + __ATOMIC_RELAXED, __ATOMIC_CONSUME, __ATOMIC_ACQUIRE, __ATOMIC_RELEASE, __ATOMIC_ACQ_REL, __ATOMIC_SEQ_CST +}; diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 0417ed9c3e9..19260f6ac24 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -112,6 +112,7 @@ void cpp_internal_additions(std::ostream &out) config.ansi_c.mode==configt::ansi_ct::flavourt::ARM) { out << "extern \"C\" {" << '\n'; + out << c2cpp(gcc_builtin_headers_types); out << c2cpp(gcc_builtin_headers_generic); out << c2cpp(gcc_builtin_headers_math); out << c2cpp(gcc_builtin_headers_mem_string);