Skip to content

C front-end: fix whitespace in built-in declarations #7587

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Mar 10, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/ansi-c/compiler_headers/gcc_builtin_headers_ia32-3.h
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ void __builtin_ia32_pmovusdw256mem_mask(__gcc_v8hi*, __gcc_v8si, unsigned char);
void __builtin_ia32_pmovusdw128mem_mask(unsigned long long int *, __gcc_v4si, unsigned char);
unsigned int __builtin_ia32_rdpkru(void);
void __builtin_ia32_wrpkru(unsigned int);
__gcc_v8si __builtin_ia32_vec_pack_sfix256 (__gcc_v4df, __gcc_v4df);
__gcc_v8si __builtin_ia32_vec_pack_sfix256(__gcc_v4df, __gcc_v4df);
unsigned short __builtin_ia32_lzcnt_u16(unsigned short);
unsigned short __builtin_ia32_tzcnt_u16(unsigned short);
unsigned int __builtin_ia32_tzcnt_u32(unsigned int);
Expand Down
10 changes: 5 additions & 5 deletions src/ansi-c/compiler_headers/gcc_builtin_headers_ia32.h
Original file line number Diff line number Diff line change
Expand Up @@ -768,7 +768,7 @@ unsigned int __builtin_ia32_rdrand32_step(unsigned int*);
unsigned int __builtin_ia32_rdrand64_step(unsigned long long int *);
void __builtin_ia32_movntsd(double*, __gcc_v2df);
void __builtin_ia32_movntss(float*, __gcc_v4sf);
__gcc_v2di __builtin_ia32_extrq (__gcc_v2di, __gcc_v16qi);
__gcc_v2di __builtin_ia32_extrq(__gcc_v2di, __gcc_v16qi);
__gcc_v2di __builtin_ia32_extrqi(__gcc_v2di, unsigned int, unsigned int);
__gcc_v2di __builtin_ia32_insertq(__gcc_v2di, __gcc_v2di);
__gcc_v2di __builtin_ia32_insertqi(__gcc_v2di, __gcc_v2di, unsigned int, unsigned int);
Expand Down Expand Up @@ -912,10 +912,10 @@ __gcc_v2df __builtin_ia32_fnmsubpd(__gcc_v2df, __gcc_v2df, __gcc_v2df);
__gcc_v4sf __builtin_ia32_fnmsubps(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf);
__gcc_v2df __builtin_ia32_fnmsubsd(__gcc_v2df, __gcc_v2df, __gcc_v2df);
__gcc_v4sf __builtin_ia32_fnmsubss(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf);
__gcc_v2df __builtin_ia32_fmaddsubpd (__gcc_v2df, __gcc_v2df, __gcc_v2df);
__gcc_v4sf __builtin_ia32_fmaddsubps (__gcc_v4sf, __gcc_v4sf, __gcc_v4sf);
__gcc_v2df __builtin_ia32_fmsubaddpd (__gcc_v2df, __gcc_v2df, __gcc_v2df);
__gcc_v4sf __builtin_ia32_fmsubaddps (__gcc_v4sf, __gcc_v4sf, __gcc_v4sf);
__gcc_v2df __builtin_ia32_fmaddsubpd(__gcc_v2df, __gcc_v2df, __gcc_v2df);
__gcc_v4sf __builtin_ia32_fmaddsubps(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf);
__gcc_v2df __builtin_ia32_fmsubaddpd(__gcc_v2df, __gcc_v2df, __gcc_v2df);
__gcc_v4sf __builtin_ia32_fmsubaddps(__gcc_v4sf, __gcc_v4sf, __gcc_v4sf);
__gcc_v4df __builtin_ia32_fmaddpd256(__gcc_v4df, __gcc_v4df, __gcc_v4df);
__gcc_v8sf __builtin_ia32_fmaddps256(__gcc_v8sf, __gcc_v8sf, __gcc_v8sf);
__gcc_v4df __builtin_ia32_fmsubpd256(__gcc_v4df, __gcc_v4df, __gcc_v4df);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ char* __builtin___strncat_chk(char*, const char*, __CPROVER_size_t, __CPROVER_si
char* __builtin___strncpy_chk(char*, const char*, __CPROVER_size_t, __CPROVER_size_t);
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 *s, __CPROVER_size_t maxlen, int flag, __CPROVER_size_t os, const char *fmt, __builtin_va_list ap);
int __builtin___vsprintf_chk(char*, int, __CPROVER_size_t, const char*, __builtin_va_list);
void* __builtin_aggregate_incoming_address();
void* __builtin_aligned_alloc(__CPROVER_size_t, __CPROVER_size_t);
Expand Down