summaryrefslogtreecommitdiff
path: root/ia32/CBuiltins.ml
Commit message (Collapse)AuthorAge
* Rename __builtin_cntlz to __builtin_clz.Gravatar xleroy2014-08-27
| | | | | | | IA32: add __builtin_clz, __builtin_ctz. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fused multiply-add for IA32.Gravatar xleroy2014-05-05
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2481 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fine hair splitting depending on whether va_list is a scalar type (IA32, ↵Gravatar xleroy2014-01-01
| | | | | | ARM) or an array type (PowerPC). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2395 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Experimental support for <stdarg.h>, the GCC way. Works on IA32. To be ↵Gravatar xleroy2014-01-01
| | | | | | tested on PowerPC and ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revert suppression of __builtin_{read,write}_reversed for x86 and ARM,Gravatar xleroy2013-04-29
| | | | | | | | for compatibility with earlier CompCert versions. But don't use them in PackedStructs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2216 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add __builtin_bswap16 and __builtin_bswap32 to all ports.Gravatar xleroy2013-04-20
| | | | | | | | | Remove __builtin_{read,write}_reversed from IA32 and ARM ports. Machregs: tighten destroyed_by_builtin Packedstructs: use bswap if read/write-reversed not available. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2208 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink: first import of Valentin Robert's validator for asm and linkGravatar xleroy2012-03-28
| | | | | | | cparser: renamed Errors to Cerrors; removed packing into Cparser. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revised emulation of packed structsGravatar xleroy2011-10-16
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1729 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM: added reversed load/store builtins + bswap builtin (to be tested)Gravatar xleroy2011-07-30
| | | | | | | | IA32: added bswap builtin Updated Changelog git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1693 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Nicer printing of annotations.Gravatar xleroy2011-05-23
| | | | | | | ia32: support builtins for reversed reads and writes (facilitates testing). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1655 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for __builtin_fmax and __builtin_fminGravatar xleroy2010-09-04
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1501 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the reuse-temps branch:Gravatar xleroy2010-09-02
- Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e