compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Support __builtin_unreachable	Xavier Leroy	2021-05-02	1	-0/+4
\| \| \| \|	Not yet used for optimizations.
*	AArch64: macOS port	Xavier Leroy	2020-12-26	1	-10/+38
\| \| \| \| \|	This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
*	Added implementation for fmin/fmax for aarch64.	Bernhard Schommer	2020-11-06	1	-0/+4
\| \| \| \| \|	The two built-in function map to the fmax and fmin instruction. Bug 30035
*	Add __builtin_sqrt as synonymous for __builtin_fsqrt	Xavier Leroy	2020-07-27	1	-1/+1
\| \| \| \|	__builtin_sqrt (no "f") is the name used by GCC and Clang.
*	AArch64 implementation of __builtin_ctz*	Xavier Leroy	2020-07-27	1	-1/+7
\| \| \| \|	Using the "rbit" instruction (reverse bits).
*	No need to process __builtin_fabs in $ARCH/Asmexpand.ml	Xavier Leroy	2020-07-27	1	-2/+0
\| \| \| \|	__builtin_fabs has already been expanded in backend/Selection.v .
*	Revert "Remove `__builtin_nop` for some architectures. (#208)"	Bernhard Schommer	2020-01-03	1	-0/+2
\| \| \| \|	This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
*	Remove `__builtin_nop` for some architectures. (#208)	Bernhard Schommer	2019-12-21	1	-2/+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.
*	The SP register has dwarf register number 31.	Bernhard Schommer	2019-12-11	1	-1/+1
\|
*	Added dwarf register numbers for aarch64	Bernhard Schommer	2019-11-28	1	-3/+18
\|
*	Offset out of range for ldp/stp instructions	xavier.leroy	2019-08-23	1	-1/+3
\| \| \| \|	These instructions are generated by __builtin_memcpy.
*	AArch64 port	Xavier Leroy	2019-08-08	1	-0/+436
	This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.