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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Ensure FunInd or Recdef is imported if functional induction is used	Sigurd Schneider	2017-07-20	1	-0/+1
\| \| \| \| \| \|	Coq 8.7 does not load FunInd in prelude anymore, so this is necessary. Recdef exports FunInd, so if Recdef is imported, importing FunInd is not required.
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-12/+12
\|
*	Updated ARM backend wrt new static analyses and optimizations.	xleroy	2014-01-02	1	-21/+32
\| \| \| \| \| \| \| \|	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
*	Updated ARM port.	xleroy	2012-07-10	1	-6/+0
\| \| \| \| \| \| \|	CSE.v: removed commented-out stuff. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1966 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update CombineOp for arm and ia32.	xleroy	2012-07-03	1	-2/+6
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1950 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Recombine x = cmp(...); if (x == 1) ...	xleroy	2012-07-01	1	-0/+29
\| \| \| \| \| \| \|	and x = cmp(...); if (x != 1) ... git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1946 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	CSE: add recognition of some combined operators, conditions, and addressing ↵	xleroy	2012-05-26	1	-0/+127
	modes (cf. CombineOp.v) Memory model: cleaning up Memdata Inlining and new Constprop: updated for ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1902 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e