Merge pull request #5918 from tautschnig/update-gcc-builtins

Update GCC builtin declarations

Author: kroening

src/ansi-c/CMakeLists.txt

@@ -63,6 +63,7 @@ make_inc(gcc_builtin_headers_ia32)
 make_inc(gcc_builtin_headers_ia32-2)
 make_inc(gcc_builtin_headers_ia32-3)
 make_inc(gcc_builtin_headers_ia32-4)
+make_inc(gcc_builtin_headers_ia32-5)
 make_inc(gcc_builtin_headers_math)
 make_inc(gcc_builtin_headers_mem_string)
 make_inc(gcc_builtin_headers_mips)
@@ -85,6 +86,7 @@ set(extra_dependencies
     ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-2.inc
     ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-3.inc
     ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-4.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32-5.inc
     ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_ia32.inc
     ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_math.inc
     ${CMAKE_CURRENT_BINARY_DIR}/gcc_builtin_headers_mem_string.inc

src/ansi-c/Makefile

@@ -58,6 +58,7 @@ BUILTIN_FILES = \
   gcc_builtin_headers_ia32-2.inc \
   gcc_builtin_headers_ia32-3.inc \
   gcc_builtin_headers_ia32-4.inc \
+  gcc_builtin_headers_ia32-5.inc \
   gcc_builtin_headers_ia32.inc \
   gcc_builtin_headers_math.inc \
   gcc_builtin_headers_mem_string.inc \

src/ansi-c/ansi_c_internal_additions.cpp

@@ -63,6 +63,9 @@ const char gcc_builtin_headers_ia32_3[]=
 const char gcc_builtin_headers_ia32_4[]=
 #include "gcc_builtin_headers_ia32-4.inc"
 ; // NOLINT(whitespace/semicolon)
+const char gcc_builtin_headers_ia32_5[] =
+#include "gcc_builtin_headers_ia32-5.inc"
+  ; // NOLINT(whitespace/semicolon)
 
 const char gcc_builtin_headers_alpha[]=
 "# 1 \"gcc_builtin_headers_alpha.h\"\n"

src/ansi-c/ansi_c_internal_additions.h

@@ -28,6 +28,7 @@ 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_ia32_5[];
 extern const char gcc_builtin_headers_alpha[];
 extern const char gcc_builtin_headers_arm[];
 extern const char gcc_builtin_headers_mips[];

src/ansi-c/arm_builtin_headers.h

@@ -1,3 +1,4 @@
+// clang-format off
 void __breakpoint(int val);
 void __cdp(unsigned int coproc, unsigned int ops, unsigned int regs);
 void __clrex(void);
@@ -41,3 +42,4 @@ int __usat(unsigned int val, unsigned int sat);
 void __wfe(void);
 void __wfi(void);
 void __yield(void);
+// clang-format on

src/ansi-c/builtin_factory.cpp

@@ -175,6 +175,9 @@ bool builtin_factory(
 
       if(find_pattern(pattern, gcc_builtin_headers_ia32_4, s))
         return convert(identifier, s, symbol_table, mh);
+
+      if(find_pattern(pattern, gcc_builtin_headers_ia32_5, s))
+        return convert(identifier, s, symbol_table, mh);
     }
     else if(config.ansi_c.arch=="arm64" ||
             config.ansi_c.arch=="armel" ||

src/ansi-c/clang_builtin_headers.h

@@ -1,8 +1,8 @@
+// clang-format off
 __gcc_v2di __builtin_ia32_undef128(void);
 __gcc_v4di __builtin_ia32_undef256(void);
 __gcc_v8di __builtin_ia32_undef512(void);
 
-// clang-format off
 __gcc_v8hi __builtin_ia32_cvtne2ps2bf16_128(__gcc_v4sf, __gcc_v4sf);
 __gcc_v16hi __builtin_ia32_cvtne2ps2bf16_256(__gcc_v8sf, __gcc_v8sf);
 __gcc_v32hi __builtin_ia32_cvtne2ps2bf16_512(__gcc_v16sf, __gcc_v16sf);
@@ -54,7 +54,6 @@ void __builtin_nontemporal_load();
 
 int __builtin_flt_rounds(void);
 
-// clang-format off
 unsigned char __builtin_rotateleft8(unsigned char, unsigned char);
 unsigned short __builtin_rotateleft16(unsigned short, unsigned short);
 unsigned int __builtin_rotateleft32(unsigned int, unsigned int);

src/ansi-c/cprover_builtin_headers.h

@@ -1,3 +1,4 @@
+// clang-format off
 void __CPROVER_assume(__CPROVER_bool assumption);
 void __VERIFIER_assume(__CPROVER_bool assumption);
 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
@@ -121,3 +122,4 @@ __CPROVER_bool __CPROVER_overflow_unary_minus();
 
 // enumerations
 __CPROVER_bool __CPROVER_enum_is_in_range();
+// clang-format on

src/ansi-c/cw_builtin_headers.h

@@ -1,3 +1,5 @@
+// clang-format off
 int __abs(int);
 void __builtin_va_info();
 __CPROVER_size_t __builtin_force_const(__CPROVER_size_t);
+// clang-format on

src/ansi-c/gcc_builtin_headers_alpha.h

@@ -1,3 +1,4 @@
+// clang-format off
 long __builtin_alpha_implver(void);
 long __builtin_alpha_rpcc(void);
 long __builtin_alpha_amask(long);
@@ -44,3 +45,4 @@ long __builtin_alpha_ctlz(long);
 long __builtin_alpha_ctpop(long);
 void *__builtin_thread_pointer(void);
 void __builtin_set_thread_pointer(void *);
+// clang-format on