replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

more gcc x86 builtins 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@1537 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2012-09-05 07:11:21 +00:00
parent 79421ec9d5
commit 9476a9d3f1
1 changed files with 15 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
src/ansi-c/gcc_builtin_headers_ia32.h
View File

@ -19,6 +19,9 @@ __gcc_v16qi __builtin_ia32_paddsb128(__gcc_v16qi,__gcc_v16qi);
__gcc_v16qi __builtin_ia32_psubsb128(__gcc_v16qi,__gcc_v16qi);
__gcc_v16qi __builtin_ia32_paddusb128(__gcc_v16qi,__gcc_v16qi);
__gcc_v16qi __builtin_ia32_psubusb128(__gcc_v16qi,__gcc_v16qi);
__gcc_di __builtin_ia32_cvtss2si64(__gcc_v4sf);
__gcc_di __builtin_ia32_cvttss2si64(__gcc_v4sf);
__gcc_v4sf __builtin_ia32_cvtsi642ss(__gcc_v4sf, __gcc_di);
// from
// http://gcc.gnu.org/onlinedocs/gcc-4.7.0/gcc/X86-Built_002din-Functions.html
@ -91,7 +94,8 @@ int __builtin_ia32_pextrw (__gcc_v4hi, int);
__gcc_v4hi __builtin_ia32_pinsrw (__gcc_v4hi, int, int);
int __builtin_ia32_pmovmskb (__gcc_v8qi);
void __builtin_ia32_maskmovq (__gcc_v8qi, __gcc_v8qi, char *);
void __builtin_ia32_movntq (__gcc_v1di *, __gcc_v1di);
//void __builtin_ia32_movntq (__gcc_v1di *, __gcc_v1di);
void __builtin_ia32_movntq (__gcc_di *, __gcc_di);
void __builtin_ia32_sfence (void);
int __builtin_ia32_comieq (__gcc_v4sf, __gcc_v4sf);
int __builtin_ia32_comineq (__gcc_v4sf, __gcc_v4sf);
@ -167,10 +171,10 @@ __gcc_v4sf __builtin_ia32_loadups (float *);
void __builtin_ia32_storeups (float *, __gcc_v4sf);
__gcc_v4sf __builtin_ia32_loadsss (float *);
void __builtin_ia32_storess (float *, __gcc_v4sf);
__gcc_v4sf __builtin_ia32_loadhps (__gcc_v4sf, const __gcc_v2si *);
__gcc_v4sf __builtin_ia32_loadlps (__gcc_v4sf, const __gcc_v2si *);
void __builtin_ia32_storehps (__gcc_v2si *, __gcc_v4sf);
void __builtin_ia32_storelps (__gcc_v2si *, __gcc_v4sf);
__gcc_v4sf __builtin_ia32_loadhps (__gcc_v4sf, const __gcc_v2sf *);
__gcc_v4sf __builtin_ia32_loadlps (__gcc_v4sf, const __gcc_v2sf *);
void __builtin_ia32_storehps (__gcc_v2sf *, __gcc_v4sf);
void __builtin_ia32_storelps (__gcc_v2sf *, __gcc_v4sf);
int __builtin_ia32_comisdeq (__gcc_v2df, __gcc_v2df);
int __builtin_ia32_comisdlt (__gcc_v2df, __gcc_v2df);
int __builtin_ia32_comisdle (__gcc_v2df, __gcc_v2df);
@ -270,7 +274,7 @@ __gcc_v2df __builtin_ia32_loadlpd (__gcc_v2df, double const *);
int __builtin_ia32_movmskpd (__gcc_v2df);
int __builtin_ia32_pmovmskb128 (__gcc_v16qi);
void __builtin_ia32_movnti (int *, int);
void __builtin_ia32_movnti64 (long long int *, long long int);
void __builtin_ia32_movnti64 (__gcc_di *, __gcc_di);
void __builtin_ia32_movntpd (double *, __gcc_v2df);
void __builtin_ia32_movntdq (__gcc_v2di *, __gcc_v2di);
__gcc_v4si __builtin_ia32_pshufd (__gcc_v4si, int);
@ -290,13 +294,13 @@ __gcc_v2si __builtin_ia32_cvttpd2pi (__gcc_v2df);
__gcc_v2df __builtin_ia32_cvtpi2pd (__gcc_v2si);
int __builtin_ia32_cvtsd2si (__gcc_v2df);
int __builtin_ia32_cvttsd2si (__gcc_v2df);
long long __builtin_ia32_cvtsd2si64 (__gcc_v2df);
long long __builtin_ia32_cvttsd2si64 (__gcc_v2df);
__gcc_di __builtin_ia32_cvtsd2si64 (__gcc_v2df);
__gcc_di __builtin_ia32_cvttsd2si64 (__gcc_v2df);
__gcc_v4si __builtin_ia32_cvtps2dq (__gcc_v4sf);
__gcc_v2df __builtin_ia32_cvtps2pd (__gcc_v4sf);
__gcc_v4si __builtin_ia32_cvttps2dq (__gcc_v4sf);
__gcc_v2df __builtin_ia32_cvtsi2sd (__gcc_v2df, int);
__gcc_v2df __builtin_ia32_cvtsi642sd (__gcc_v2df, long long);
__gcc_v2df __builtin_ia32_cvtsi642sd (__gcc_v2df, __gcc_di);
__gcc_v4sf __builtin_ia32_cvtsd2ss (__gcc_v4sf, __gcc_v2df);
__gcc_v2df __builtin_ia32_cvtss2sd (__gcc_v2df, __gcc_v4sf);
void __builtin_ia32_clflush (const void *);
@ -418,10 +422,10 @@ __gcc_v4sf __builtin_ia32_vec_set___gcc_v4sf (__gcc_v4sf, float, const int);
int __builtin_ia32_vec_ext___gcc_v16qi (__gcc_v16qi, const int);
__gcc_v16qi __builtin_ia32_vec_set___gcc_v16qi (__gcc_v16qi, int, const int);
__gcc_v4si __builtin_ia32_vec_set___gcc_v4si (__gcc_v4si, int, const int);
__gcc_v2di __builtin_ia32_vec_set___gcc_v2di (__gcc_v2di, long long, const int);
__gcc_v2di __builtin_ia32_vec_set___gcc_v2di (__gcc_v2di, __gcc_di, const int);
float __builtin_ia32_vec_ext___gcc_v4sf (__gcc_v4sf, const int);
int __builtin_ia32_vec_ext___gcc_v4si (__gcc_v4si, const int);
long long __builtin_ia32_vec_ext___gcc_v2di (__gcc_v2di, const int);
__gcc_di __builtin_ia32_vec_ext___gcc_v2di (__gcc_v2di, const int);
__gcc_v16qi __builtin_ia32_pcmpestrm128 (__gcc_v16qi, int, __gcc_v16qi, int, const int);
int __builtin_ia32_pcmpestri128 (__gcc_v16qi, int, __gcc_v16qi, int, const int);
int __builtin_ia32_pcmpestria128 (__gcc_v16qi, int, __gcc_v16qi, int, const int);