compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Replace `omega` tactic with `lia`	Xavier Leroy	2020-12-29	1	-1/+1
\| \| \| \| \| \| \| \| \| \| \|	Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
*	AArch64 modeling of registers destroyed by pseudo-instructions	Xavier Leroy	2020-12-06	1	-4/+4
\| \| \| \| \| \|	Pfmovimms, Pfmovimmd destroy X16 Pbtbl preserves X17 Inlined built-in functions destroy X16 and X30
*	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
*	AArch64 implementation of __builtin_ctz*	Xavier Leroy	2020-07-27	1	-0/+2
\| \| \| \|	Using the "rbit" instruction (reverse bits).
*	Revert "Remove `__builtin_nop` for some architectures. (#208)"	Bernhard Schommer	2020-01-03	1	-1/+3
\| \| \| \|	This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
*	Remove `__builtin_nop` for some architectures. (#208)	Bernhard Schommer	2019-12-21	1	-3/+1
\| \| \| \| \| \| \|	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.
*	AArch64 port	Xavier Leroy	2019-08-08	1	-0/+1312
	This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.