compcert-kvx - Unnamed repository; edit this file 'description' to name the repository.

	Commit message (Collapse)	Author	Age	Files	Lines
*	[BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵	Cyril SIX	2021-06-01	1	-4/+5
\| \| \| \|	cfrontend/C2C.ml
*	Support Cygwin 64 bits	Xavier Leroy	2020-10-05	1	-2/+6
\| \| \| \| \| \|	- Add support for the Win64 ABI to the x86_64 port - Update vararg support to handle Win64 conventions - Configure support for x86_64-cygwin64
*	Move declarations of __builtin_clz* and __builtin_ctz* to C2C.ml	Xavier Leroy	2020-07-27	1	-13/+0
\| \| \| \|	These functions are now available on all targets.
*	Remove __builtin_nop from list of x86 builtins.	Bernhard Schommer	2020-01-03	1	-3/+0
\|
*	Revert "Remove `__builtin_nop` for some architectures. (#208)"	Bernhard Schommer	2020-01-03	1	-0/+3
\| \| \| \|	This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
*	Remove `__builtin_nop` for some architectures. (#208)	Bernhard Schommer	2019-12-21	1	-3/+0
\| \| \| \| \| \| \|	The `__builtin_nop` function is documented only for PowerPC. It was added to the other architectures by copy paste, but has no known uses. So, remove `__builtin_nop` from all architectures but PowerPC.
*	bswap builtins: give semantics to them, support bswap64 on all targets	Bernhard Schommer	2019-08-12	1	-2/+0
\| \| \| \| \| \| \| \| \| \| \| \|	* Added semantic for byte swap builtins The `__builtin_bswap`, `__builtin_bswap16`, `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics. The semantics is given in terms of the decode/encode functions used for the memory model. * Added bswap64 expansion to PowerPC 32 bits. * Added bswap64 expansion for ARM.
*	Remove the cparser/Builtins module	Xavier Leroy	2019-07-17	1	-2/+2
\| \| \| \| \| \| \| \| \|	Move its definitions to modules C (the type `builtins`) and Env (the operations that deal with the initial environment). Reasons for the refactoring: 1- The name "Builtins" will soon be reused for a Coq module 2- `Env.initial()` makes more sense than `Builtins.environment()`.
*	Moved common buitlins to C2C gernic_builtins.	Bernhard Schommer	2017-09-26	1	-8/+0
\|
*	Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵	Xavier Leroy	2016-10-27	1	-0/+94
	-> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).