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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge branch 'master' into merge_master_8.13.1	Sylvain Boulmé	2021-03-23	1	-3/+3
\|\ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
\| *	Replace `omega` tactic with `lia`	Xavier Leroy	2020-12-29	1	-3/+3
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	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`.
* \|	Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵	David Monniaux	2019-06-03	1	-5/+5
\|\\| \| \| \| \| \| \|	mppa-if-conversion
\| *	Move Z definitions out of Integers and into Zbits	Xavier Leroy	2019-04-26	1	-5/+5
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The module Integers.Make contained lots of definitions and theorems about Z integers that were independent of the word size. These definitions and theorems are useful outside Integers.Make, but it felt unnatural to fetch them from modules Int or Int64. This commit moves the word-size-independent definitions and theorems to a new module, lib/Zbits.v, and fixes their uses in the code base.
* \|	seems like powerpc runs but the result segfaults	David Monniaux	2019-03-22	1	-0/+1
\|/
*	Constprop strength reduction (#17)	Bernhard Schommer	2017-07-12	1	-16/+2
\| \| \| \| \| \| \|	PowerPC port: add strength reduction for 64-bit operations * Added strength reduction for 64bit compare, subl, addl, mull, andl, orl, xorl, divl, shll, shrl, shrlu, shrluimm, shllimm, mullimm, divlu. (Bug 21748) * Moved shru_rolml proof to Values.
*	Hybrid 64bit/32bit PowerPC port	Bernhard Schommer	2017-05-03	1	-2/+623
\| \| \| \| \| \| \| \| \| \| \| \| \|	This commit adds code generation for 64bit PowerPC architectures which execute 32bit applications. The main difference to the normal 32bit PowerPC port is that it uses the available 64bit instructions instead of using the runtime library functions. However pointers are still 32bit and the 32bit calling convention is used. In order to use this port the target architecture must be either in Server execution mode or if in Embedded execution mode the high order 32 bits of GPRs must be implemented in 32-bit mode. Furthermore the operating system must preserve the high order 32 bits of GPRs.
*	Support for 64-bit architectures: update the PowerPC port	Xavier Leroy	2016-10-01	1	-0/+22
	The PowerPC port remains 32-bit only, no support is added for PPC 64. This shows how much work is needed to update an existing port a minima.