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

src/ansi-c/gcc_builtin_headers_arm.h

@@ -1,3 +1,4 @@
+// clang-format off
 int __builtin_arm_getwcx(int);
 void __builtin_arm_setwcx(int, int);
 int __builtin_arm_textrmsb(__gcc_v8qi, int);
@@ -132,3 +133,4 @@ __gcc_v4hi __builtin_arm_wunpckilh(__gcc_v4hi, __gcc_v4hi);
 __gcc_v2si __builtin_arm_wunpckilw(__gcc_v2si, __gcc_v2si);
 long long __builtin_arm_wxor(long long, long long);
 long long __builtin_arm_wzero();
+// clang-format on

src/ansi-c/gcc_builtin_headers_generic.h

@@ -1,5 +1,7 @@
+// clang-format off
 // stdarg
 void* __builtin_apply_args();
+void* __builtin_apply(void (*)(), void*, __CPROVER_size_t);
 void __builtin_ms_va_end(void *ap);
 void __builtin_ms_va_start(void *ap, ...);
 void* __builtin_next_arg();
@@ -20,46 +22,7 @@ int __builtin_execv(const char*, const char**);
 int __builtin_execve(const char*, const char**, const char**);
 int __builtin_execvp(const char*, const char**);
 void __builtin_exit(int);
-
-// stdio
-int __builtin___fprintf_chk(void*, int, const char*, ...);
-int __builtin___printf_chk(int, const char*, ...);
-int __builtin___snprintf_chk(char*, __CPROVER_size_t, int, __CPROVER_size_t, const char*, ...);
-int __builtin___sprintf_chk(char*, int, __CPROVER_size_t, const char*, ...);
-int __builtin___vfprintf_chk(void*, int, const char*, __builtin_va_list);
-int __builtin___vprintf_chk(int, const char*, __builtin_va_list);
-int __builtin___vsnprintf_chk (char *s, __CPROVER_size_t maxlen, int flag, __CPROVER_size_t os, const char *fmt, __builtin_va_list ap);
-int __builtin___vsnprintf_chk(char*, __CPROVER_size_t, int, __CPROVER_size_t, const char*, __builtin_va_list);
-int __builtin___vsprintf_chk(char*, int, __CPROVER_size_t, const char*, __builtin_va_list);
-long __builtin_expect(long, long);
-int __builtin_fprintf(void *stream, const char *fmt, ...);
-int __builtin_fprintf_unlocked(void*, const char*, ...);
-int __builtin_fputc(int, void*);
-int __builtin_fputc_unlocked(int, void*);
-int __builtin_fputs(const char *s, void *stream);
-int __builtin_fputs_unlocked(const char*, void*);
-int __builtin_fscanf(void *stream, const char *fmt, ...);
-__CPROVER_size_t __builtin_fwrite(const void*, __CPROVER_size_t, __CPROVER_size_t, void*);
-__CPROVER_size_t __builtin_fwrite_unlocked(const void*, __CPROVER_size_t, __CPROVER_size_t, void*);
-int __builtin_printf(const char*, ...);
-int __builtin_printf_unlocked(const char*, ...);
-int __builtin_putc(int, void*);
-int __builtin_putc_unlocked(int, void*);
-int __builtin_putchar(int);
-int __builtin_putchar_unlocked(int);
-int __builtin_puts(const char*);
-int __builtin_puts_unlocked(const char*);
-int __builtin_scanf(const char *str, const char *fmt, ...);
-int __builtin_snprintf(char*, __CPROVER_size_t, const char*, ...);
-int __builtin_sprintf(char*, const char*, ...);
-int __builtin_sscanf(const char*, const char*, ...);
-int __builtin_vfprintf(void*, const char*, __builtin_va_list);
-int __builtin_vfscanf(void*, const char*, __builtin_va_list);
-int __builtin_vprintf(const char*, __builtin_va_list);
-int __builtin_vscanf(const char*, __builtin_va_list);
-int __builtin_vsnprintf(char*, __CPROVER_size_t, const char*, __builtin_va_list);
-int __builtin_vsprintf(char*, const char*, __builtin_va_list);
-int __builtin_vsscanf(const char*, const char*, __builtin_va_list);
+pid_t __builtin_fork();
 
 // atomics
 void __sync_synchronize();
@@ -76,11 +39,16 @@ int __builtin_classify_type();
 int __builtin_constant_p(int);
 void __builtin_trap(void);
 void __builtin_unreachable(void);
+long __builtin_expect(long, long);
+long __builtin_expect_with_probability(long, long, double);
+void __builtin_clear_padding();
+void __builtin_speculation_safe_value();
+void* __builtin_speculation_safe_value_ptr(void*, ...);
 
 void* __builtin_dwarf_cfa();
 unsigned __builtin_dwarf_sp_column();
 int __builtin_eh_return_data_regno(int);
-void __builtin_init_dwarf_reg___CPROVER_size_table(void*);
+void __builtin_init_dwarf_reg_size_table(void*);
 void __builtin_unwind_init();
 
 const char* __builtin_FILE();
@@ -92,3 +60,4 @@ void __builtin_return(void*);
 void* __builtin_saveregs();
 int __builtin_setjmp(void*);
 void __builtin_update_setjmp_buf(void*);
+// clang-format on

src/ansi-c/gcc_builtin_headers_ia32-2.h

@@ -1,3 +1,4 @@
+// clang-format off
 void __builtin_ia32_emms();
 __gcc_v2si __builtin_ia32_pmaddwd(__gcc_v4hi, __gcc_v4hi);
 __gcc_v2si __builtin_ia32_vec_init_v2si(int, int);
@@ -93,9 +94,9 @@ void __builtin_ia32_pmovqw512mem_mask(__gcc_v8hi*, __gcc_v8di, unsigned char);
 void __builtin_ia32_pmovusdw512mem_mask(__gcc_v16hi*, __gcc_v16si, unsigned short);
 void __builtin_ia32_pmovsdw512mem_mask(__gcc_v16hi*, __gcc_v16si, unsigned short);
 void __builtin_ia32_pmovdw512mem_mask(__gcc_v16hi*, __gcc_v16si, unsigned short);
-void __builtin_ia32_pmovqb512mem_mask(__gcc_v16qi*, __gcc_v8di, unsigned char);
-void __builtin_ia32_pmovusqb512mem_mask(__gcc_v16qi*, __gcc_v8di, unsigned char);
-void __builtin_ia32_pmovsqb512mem_mask(__gcc_v16qi*, __gcc_v8di, unsigned char);
+void __builtin_ia32_pmovqb512mem_mask(unsigned long long*, __gcc_v8di, unsigned char);
+void __builtin_ia32_pmovusqb512mem_mask(unsigned long long*, __gcc_v8di, unsigned char);
+void __builtin_ia32_pmovsqb512mem_mask(unsigned long long*, __gcc_v8di, unsigned char);
 void __builtin_ia32_pmovusdb512mem_mask(__gcc_v16qi*, __gcc_v16si, unsigned short);
 void __builtin_ia32_pmovsdb512mem_mask(__gcc_v16qi*, __gcc_v16si, unsigned short);
 void __builtin_ia32_pmovdb512mem_mask(__gcc_v16qi*, __gcc_v16si, unsigned short);
@@ -128,36 +129,36 @@ __gcc_v4sf __builtin_ia32_copysignps(__gcc_v4sf, __gcc_v4sf);
 float __builtin_ia32_rsqrtf(float);
 __gcc_v2df __builtin_ia32_copysignpd(__gcc_v2df, __gcc_v2df);
 __gcc_v4si __builtin_ia32_vec_pack_sfix(__gcc_v2df, __gcc_v2df);
-__gcc_v2df __builtin_ia32_floorpd(__gcc_v2df, const int);
-__gcc_v2df __builtin_ia32_ceilpd(__gcc_v2df, const int);
-__gcc_v2df __builtin_ia32_truncpd(__gcc_v2df, const int);
+__gcc_v2df __builtin_ia32_floorpd(__gcc_v2df);
+__gcc_v2df __builtin_ia32_ceilpd(__gcc_v2df);
+__gcc_v2df __builtin_ia32_truncpd(__gcc_v2df);
 __gcc_v2df __builtin_ia32_rintpd(__gcc_v2df, const int);
-__gcc_v4si __builtin_ia32_floorpd_vec_pack_sfix(__gcc_v2df, __gcc_v2df, const int);
-__gcc_v4si __builtin_ia32_ceilpd_vec_pack_sfix(__gcc_v2df, __gcc_v2df, const int);
+__gcc_v4si __builtin_ia32_floorpd_vec_pack_sfix(__gcc_v2df, __gcc_v2df);
+__gcc_v4si __builtin_ia32_ceilpd_vec_pack_sfix(__gcc_v2df, __gcc_v2df);
 __gcc_v2df __builtin_ia32_roundpd_az(__gcc_v2df);
 __gcc_v4si __builtin_ia32_roundpd_az_vec_pack_sfix(__gcc_v2df, __gcc_v2df);
-__gcc_v4sf __builtin_ia32_floorps(__gcc_v4sf, const int);
-__gcc_v4sf __builtin_ia32_ceilps(__gcc_v4sf, const int);
-__gcc_v4sf __builtin_ia32_truncps(__gcc_v4sf, const int);
+__gcc_v4sf __builtin_ia32_floorps(__gcc_v4sf);
+__gcc_v4sf __builtin_ia32_ceilps(__gcc_v4sf);
+__gcc_v4sf __builtin_ia32_truncps(__gcc_v4sf);
 __gcc_v4sf __builtin_ia32_rintps(__gcc_v4sf, const int);
-__gcc_v4si __builtin_ia32_floorps_sfix(__gcc_v4sf, const int);
-__gcc_v4si __builtin_ia32_ceilps_sfix(__gcc_v4sf, const int);
+__gcc_v4si __builtin_ia32_floorps_sfix(__gcc_v4sf);
+__gcc_v4si __builtin_ia32_ceilps_sfix(__gcc_v4sf);
 __gcc_v4sf __builtin_ia32_roundps_az(__gcc_v4sf);
 __gcc_v4si __builtin_ia32_roundps_az_sfix(__gcc_v4sf);
-__gcc_v4df __builtin_ia32_floorpd256(__gcc_v4df, const int);
-__gcc_v4df __builtin_ia32_ceilpd256(__gcc_v4df, const int);
-__gcc_v4df __builtin_ia32_truncpd256(__gcc_v4df, const int);
+__gcc_v4df __builtin_ia32_floorpd256(__gcc_v4df);
+__gcc_v4df __builtin_ia32_ceilpd256(__gcc_v4df);
+__gcc_v4df __builtin_ia32_truncpd256(__gcc_v4df);
 __gcc_v4df __builtin_ia32_rintpd256(__gcc_v4df, const int);
 __gcc_v4df __builtin_ia32_roundpd_az256(__gcc_v4df);
 __gcc_v8si __builtin_ia32_roundpd_az_vec_pack_sfix256(__gcc_v4df, __gcc_v4df);
-__gcc_v8si __builtin_ia32_floorpd_vec_pack_sfix256(__gcc_v4df, __gcc_v4df, const int);
-__gcc_v8si __builtin_ia32_ceilpd_vec_pack_sfix256(__gcc_v4df, __gcc_v4df, const int);
-__gcc_v8sf __builtin_ia32_floorps256(__gcc_v8sf, const int);
-__gcc_v8sf __builtin_ia32_ceilps256(__gcc_v8sf, const int);
-__gcc_v8sf __builtin_ia32_truncps256(__gcc_v8sf, const int);
+__gcc_v8si __builtin_ia32_floorpd_vec_pack_sfix256(__gcc_v4df, __gcc_v4df);
+__gcc_v8si __builtin_ia32_ceilpd_vec_pack_sfix256(__gcc_v4df, __gcc_v4df);
+__gcc_v8sf __builtin_ia32_floorps256(__gcc_v8sf);
+__gcc_v8sf __builtin_ia32_ceilps256(__gcc_v8sf);
+__gcc_v8sf __builtin_ia32_truncps256(__gcc_v8sf);
 __gcc_v8sf __builtin_ia32_rintps256(__gcc_v8sf, const int);
-__gcc_v8si __builtin_ia32_floorps_sfix256(__gcc_v8sf, const int);
-__gcc_v8si __builtin_ia32_ceilps_sfix256(__gcc_v8sf, const int);
+__gcc_v8si __builtin_ia32_floorps_sfix256(__gcc_v8sf);
+__gcc_v8si __builtin_ia32_ceilps_sfix256(__gcc_v8sf);
 __gcc_v8sf __builtin_ia32_roundps_az256(__gcc_v8sf);
 __gcc_v8si __builtin_ia32_roundps_az_sfix256(__gcc_v8sf);
 __gcc_v8sf __builtin_ia32_copysignps256(__gcc_v8sf, __gcc_v8sf);
@@ -196,7 +197,7 @@ __gcc_v16si __builtin_ia32_broadcasti32x4_512(__gcc_v4si, __gcc_v16si, unsigned
 __gcc_v8di __builtin_ia32_broadcasti64x4_512(__gcc_v4di, __gcc_v8di, unsigned char);
 __gcc_v8df __builtin_ia32_broadcastsd512(__gcc_v2df, __gcc_v8df, unsigned char);
 __gcc_v16sf __builtin_ia32_broadcastss512(__gcc_v4sf, __gcc_v16sf, unsigned short);
-short __builtin_ia32_cmpd512_mask(__gcc_v16si, __gcc_v16si, int, short);
+unsigned short __builtin_ia32_cmpd512_mask(__gcc_v16si, __gcc_v16si, int, unsigned short);
 unsigned char __builtin_ia32_cmpq512_mask(__gcc_v8di, __gcc_v8di, int, unsigned char);
 __gcc_v8df __builtin_ia32_compressdf512_mask(__gcc_v8df, __gcc_v8df, unsigned char);
 __gcc_v16sf __builtin_ia32_compresssf512_mask(__gcc_v16sf, __gcc_v16sf, unsigned short);
@@ -295,22 +296,22 @@ __gcc_v8di __builtin_ia32_prorq512_mask(__gcc_v8di, int, __gcc_v8di, unsigned ch
 __gcc_v16si __builtin_ia32_prorvd512_mask(__gcc_v16si, __gcc_v16si, __gcc_v16si, unsigned short);
 __gcc_v8di __builtin_ia32_prorvq512_mask(__gcc_v8di, __gcc_v8di, __gcc_v8di, unsigned char);
 __gcc_v16si __builtin_ia32_pshufd512_mask(__gcc_v16si, int, __gcc_v16si, unsigned short);
-__gcc_v16si __builtin_ia32_pslld512_mask(__gcc_v16si, __gcc_v4si, __gcc_v16si, short);
-__gcc_v16si __builtin_ia32_pslldi512_mask(__gcc_v16si, int, __gcc_v16si, short);
-__gcc_v8di __builtin_ia32_psllq512_mask(__gcc_v8di, __gcc_v2di, __gcc_v8di, char);
-__gcc_v8di __builtin_ia32_psllqi512_mask(__gcc_v8di, int, __gcc_v8di, char);
+__gcc_v16si __builtin_ia32_pslld512_mask(__gcc_v16si, __gcc_v4si, __gcc_v16si, unsigned short);
+__gcc_v16si __builtin_ia32_pslldi512_mask(__gcc_v16si, int, __gcc_v16si, unsigned short);
+__gcc_v8di __builtin_ia32_psllq512_mask(__gcc_v8di, __gcc_v2di, __gcc_v8di, unsigned char);
+__gcc_v8di __builtin_ia32_psllqi512_mask(__gcc_v8di, int, __gcc_v8di, unsigned char);
 __gcc_v16si __builtin_ia32_psllv16si_mask(__gcc_v16si, __gcc_v16si, __gcc_v16si, unsigned short);
 __gcc_v8di __builtin_ia32_psllv8di_mask(__gcc_v8di, __gcc_v8di, __gcc_v8di, unsigned char);
-__gcc_v16si __builtin_ia32_psrad512_mask(__gcc_v16si, __gcc_v4si, __gcc_v16si, short);
-__gcc_v16si __builtin_ia32_psradi512_mask(__gcc_v16si, int, __gcc_v16si, short);
-__gcc_v8di __builtin_ia32_psraq512_mask(__gcc_v8di, __gcc_v2di, __gcc_v8di, char);
-__gcc_v8di __builtin_ia32_psraqi512_mask(__gcc_v8di, int, __gcc_v8di, char);
+__gcc_v16si __builtin_ia32_psrad512_mask(__gcc_v16si, __gcc_v4si, __gcc_v16si, unsigned short);
+__gcc_v16si __builtin_ia32_psradi512_mask(__gcc_v16si, int, __gcc_v16si, unsigned short);
+__gcc_v8di __builtin_ia32_psraq512_mask(__gcc_v8di, __gcc_v2di, __gcc_v8di, unsigned char);
+__gcc_v8di __builtin_ia32_psraqi512_mask(__gcc_v8di, int, __gcc_v8di, unsigned char);
 __gcc_v16si __builtin_ia32_psrav16si_mask(__gcc_v16si, __gcc_v16si, __gcc_v16si, unsigned short);
 __gcc_v8di __builtin_ia32_psrav8di_mask(__gcc_v8di, __gcc_v8di, __gcc_v8di, unsigned char);
-__gcc_v16si __builtin_ia32_psrld512_mask(__gcc_v16si, __gcc_v4si, __gcc_v16si, short);
-__gcc_v16si __builtin_ia32_psrldi512_mask(__gcc_v16si, int, __gcc_v16si, short);
-__gcc_v8di __builtin_ia32_psrlq512_mask(__gcc_v8di, __gcc_v2di, __gcc_v8di, char);
-__gcc_v8di __builtin_ia32_psrlqi512_mask(__gcc_v8di, int, __gcc_v8di, char);
+__gcc_v16si __builtin_ia32_psrld512_mask(__gcc_v16si, __gcc_v4si, __gcc_v16si, unsigned short);
+__gcc_v16si __builtin_ia32_psrldi512_mask(__gcc_v16si, int, __gcc_v16si, unsigned short);
+__gcc_v8di __builtin_ia32_psrlq512_mask(__gcc_v8di, __gcc_v2di, __gcc_v8di, unsigned char);
+__gcc_v8di __builtin_ia32_psrlqi512_mask(__gcc_v8di, int, __gcc_v8di, unsigned char);
 __gcc_v16si __builtin_ia32_psrlv16si_mask(__gcc_v16si, __gcc_v16si, __gcc_v16si, unsigned short);
 __gcc_v8di __builtin_ia32_psrlv8di_mask(__gcc_v8di, __gcc_v8di, __gcc_v8di, unsigned char);
 __gcc_v16si __builtin_ia32_psubd512_mask(__gcc_v16si, __gcc_v16si, __gcc_v16si, unsigned short);
@@ -339,7 +340,7 @@ __gcc_v16sf __builtin_ia32_shuf_f32x4_mask(__gcc_v16sf, __gcc_v16sf, int, __gcc_
 __gcc_v8df __builtin_ia32_shuf_f64x2_mask(__gcc_v8df, __gcc_v8df, int, __gcc_v8df, unsigned char);
 __gcc_v16si __builtin_ia32_shuf_i32x4_mask(__gcc_v16si, __gcc_v16si, int, __gcc_v16si, unsigned short);
 __gcc_v8di __builtin_ia32_shuf_i64x2_mask(__gcc_v8di, __gcc_v8di, int, __gcc_v8di, unsigned char);
-short __builtin_ia32_ucmpd512_mask(__gcc_v16si, __gcc_v16si, int, short);
+unsigned short __builtin_ia32_ucmpd512_mask(__gcc_v16si, __gcc_v16si, int, unsigned short);
 unsigned char __builtin_ia32_ucmpq512_mask(__gcc_v8di, __gcc_v8di, int, unsigned char);
 __gcc_v8df __builtin_ia32_unpckhpd512_mask(__gcc_v8df, __gcc_v8df, __gcc_v8df, unsigned char);
 __gcc_v16sf __builtin_ia32_unpckhps512_mask(__gcc_v16sf, __gcc_v16sf, __gcc_v16sf, unsigned short);
@@ -381,8 +382,8 @@ __gcc_v8df __builtin_ia32_sqrtpd512(__gcc_v8df, ...);
 __gcc_v16sf __builtin_ia32_sqrtps512(__gcc_v16sf, ...);
 __gcc_v16sf __builtin_ia32_exp2ps(__gcc_v16sf);
 __gcc_v16si __builtin_ia32_roundpd_az_vec_pack_sfix512(__gcc_v8df, __gcc_v8df);
-__gcc_v16si __builtin_ia32_floorpd_vec_pack_sfix512(__gcc_v8df, __gcc_v8df, const int);
-__gcc_v16si __builtin_ia32_ceilpd_vec_pack_sfix512(__gcc_v8df, __gcc_v8df, const int);
+__gcc_v16si __builtin_ia32_floorpd_vec_pack_sfix512(__gcc_v8df, __gcc_v8df);
+__gcc_v16si __builtin_ia32_ceilpd_vec_pack_sfix512(__gcc_v8df, __gcc_v8df);
 unsigned short __builtin_ia32_kandhi(unsigned short, unsigned short);
 unsigned short __builtin_ia32_kandnhi(unsigned short, unsigned short);
 unsigned short __builtin_ia32_knothi(unsigned short);
@@ -651,3 +652,4 @@ void __builtin_ia32_scatterpfdpd(char, __gcc_v8si,const long*, int, int);
 void __builtin_ia32_scatterpfdps( short, __gcc_v16si, const int*, int, int);
 void __builtin_ia32_scatterpfqpd(char, __gcc_v8di,const long*, int, int);
 void __builtin_ia32_scatterpfqps(char, __gcc_v8di, const int*, int, int);
+// clang-format on