compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Remove coq warnings (#28)	Bernhard Schommer	2017-09-22	1	-6/+6
\| \| \| \|	Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
*	Subst's behavior on let-ins has changed.	Maxime Dénès	2017-01-09	1	-2/+2
\|
*	Support for 64-bit architectures: generic support	Xavier Leroy	2016-10-01	1	-31/+33
\| \| \| \| \| \| \| \| \| \| \|	- Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
*	Improved handling of "rotate left" and "rotate right" operators	Xavier Leroy	2016-06-22	1	-17/+27
\| \| \| \| \| \| \| \|	- Values: "rol" and "ror" are defined even if their second argument is not in the [0,31] range (for consistency with "rolm" and because the semantics is definitely well defined in this case). - NeedDomain: more precise analysis of "rol" and "rolm", could benefit the PowerPC port.
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-160/+160
\|
*	Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵	Xavier Leroy	2015-04-30	1	-2/+2
\| \| \| \|	Val.lessdef, etc.
*	Verification of the Unusedglob pass (removal of unreferenced static global ↵	Xavier Leroy	2014-11-24	1	-4/+4
\| \| \| \|	definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-84/+17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	- Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4.	xleroy	2014-01-12	1	-1/+0
\| \| \| \| \| \| \|	- Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated neededness analysis for IA32.	xleroy	2014-01-02	1	-1/+14
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2400 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated ARM backend wrt new static analyses and optimizations.	xleroy	2014-01-02	1	-25/+26
\| \| \| \| \| \| \| \|	NeedOp, Deadcode: must have distinct needs per argument of an operator. This change remains to be propagated to IA32 and PPC. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2399 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of branch value-analysis.	xleroy	2013-12-20	1	-0/+1515
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e