|
4 | 4 |
|
5 | 5 | __CPROVER_Float128 __builtin_fabsq(__CPROVER_Float128); |
6 | 6 | __CPROVER_Float128 __builtin_copysignq(__CPROVER_Float128, __CPROVER_Float128); |
7 | | -void __builtin_ia32_pause(); |
| 7 | +void __builtin_ia32_pause(void); |
8 | 8 | __CPROVER_Float128 __builtin_infq(void); |
9 | 9 | __CPROVER_Float128 __builtin_huge_valq(void); |
10 | 10 | __gcc_v8qi __builtin_ia32_paddb(__gcc_v8qi, __gcc_v8qi); |
@@ -82,7 +82,7 @@ void __builtin_ia32_maskmovq(__gcc_v8qi, __gcc_v8qi, char*); |
82 | 82 | // So, we use: |
83 | 83 | void __builtin_ia32_movntq(void*, ...); |
84 | 84 |
|
85 | | -void __builtin_ia32_sfence(); |
| 85 | +void __builtin_ia32_sfence(void); |
86 | 86 | int __builtin_ia32_comieq(__gcc_v4sf, __gcc_v4sf); |
87 | 87 | int __builtin_ia32_comineq(__gcc_v4sf, __gcc_v4sf); |
88 | 88 | int __builtin_ia32_comilt(__gcc_v4sf, __gcc_v4sf); |
@@ -309,7 +309,7 @@ __gcc_v2df __builtin_ia32_cvtsi642sd(__gcc_v2df, long long); |
309 | 309 | __gcc_v4sf __builtin_ia32_cvtsd2ss(__gcc_v4sf, __gcc_v2df); |
310 | 310 | __gcc_v2df __builtin_ia32_cvtss2sd(__gcc_v2df, __gcc_v4sf); |
311 | 311 | void __builtin_ia32_clflush(const void*); |
312 | | -void __builtin_ia32_lfence(); |
| 312 | +void __builtin_ia32_lfence(void); |
313 | 313 | void __builtin_ia32_mfence(void); |
314 | 314 | __gcc_v16qi __builtin_ia32_loaddqu(const char*); |
315 | 315 | void __builtin_ia32_storedqu(char*, __gcc_v16qi); |
@@ -573,8 +573,8 @@ int __builtin_ia32_vtestzpd(__gcc_v2df, __gcc_v2df); |
573 | 573 | int __builtin_ia32_vtestzpd256(__gcc_v4df, __gcc_v4df); |
574 | 574 | int __builtin_ia32_vtestzps(__gcc_v4sf, __gcc_v4sf); |
575 | 575 | int __builtin_ia32_vtestzps256(__gcc_v8sf, __gcc_v8sf); |
576 | | -void __builtin_ia32_vzeroall(); |
577 | | -void __builtin_ia32_vzeroupper(); |
| 576 | +void __builtin_ia32_vzeroall(void); |
| 577 | +void __builtin_ia32_vzeroupper(void); |
578 | 578 | __gcc_v4df __builtin_ia32_xorpd256(__gcc_v4df, __gcc_v4df); |
579 | 579 | __gcc_v8sf __builtin_ia32_xorps256(__gcc_v8sf, __gcc_v8sf); |
580 | 580 | __gcc_v32qi __builtin_ia32_mpsadbw256(__gcc_v32qi, __gcc_v32qi, int); |
@@ -755,10 +755,10 @@ __gcc_v2di __builtin_ia32_aesdeclast128(__gcc_v2di, __gcc_v2di); |
755 | 755 | __gcc_v2di __builtin_ia32_aeskeygenassist128(__gcc_v2di, const int); |
756 | 756 | __gcc_v2di __builtin_ia32_aesimc128(__gcc_v2di); |
757 | 757 | __gcc_v2di __builtin_ia32_pclmulqdq128(__gcc_v2di, __gcc_v2di, const int); |
758 | | -unsigned __builtin_ia32_rdfsbase32(); |
759 | | -unsigned long long __builtin_ia32_rdfsbase64(); |
760 | | -unsigned __builtin_ia32_rdgsbase32(); |
761 | | -unsigned long long __builtin_ia32_rdgsbase64(); |
| 758 | +unsigned __builtin_ia32_rdfsbase32(void); |
| 759 | +unsigned long long __builtin_ia32_rdfsbase64(void); |
| 760 | +unsigned __builtin_ia32_rdgsbase32(void); |
| 761 | +unsigned long long __builtin_ia32_rdgsbase64(void); |
762 | 762 | void _writefsbase_u32(unsigned int); |
763 | 763 | void _writefsbase_u64(unsigned long long); |
764 | 764 | void _writegsbase_u32(unsigned int); |
@@ -953,7 +953,7 @@ unsigned __builtin_ia32_lzcnt_u32(unsigned); |
953 | 953 | unsigned long long __builtin_ia32_lzcnt_u64(unsigned long long); |
954 | 954 | unsigned __builtin_ia32_bextri_u32(unsigned, unsigned); |
955 | 955 | unsigned long long __builtin_ia32_bextri_u64(unsigned long long, unsigned long long); |
956 | | -void __builtin_ia32_femms(); |
| 956 | +void __builtin_ia32_femms(void); |
957 | 957 | __gcc_v8qi __builtin_ia32_pavgusb(__gcc_v8qi, __gcc_v8qi); |
958 | 958 | __gcc_v2si __builtin_ia32_pf2id(__gcc_v2sf); |
959 | 959 | __gcc_v2sf __builtin_ia32_pfacc(__gcc_v2sf, __gcc_v2sf); |
|
0 commit comments