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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Refine the type of function results in AST.signature	Xavier Leroy	2020-02-21	1	-1/+1
\| \| \| \| \| \| \| \| \| \|	Before it was "option typ". Now it is a proper inductive type that can also express small integer types (8/16-bit unsigned/signed integers). One benefit is that external functions get more precise types that control better their return values. As a consequence, the CompCert C type preservation property now holds unconditionally, without extra typing hypotheses on external functions.
*	Update the back-end proofs to the new linking framework.	Xavier Leroy	2016-03-06	1	-9/+2
\|
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-2/+2
\|
*	Add flags to control individual optimization passes + flag -O0 for turning ↵	Xavier Leroy	2014-11-16	1	-2/+1
\| \| \| \|	them off.
*	Add option -Os to optimize for code size rather than for execution speed.	xleroy	2014-02-19	1	-2/+1
\| \| \| \| \| \| \| \|	Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Add option -fno-tailcalls to turn off tailcall elimination (causes problem ↵	xleroy	2013-05-17	1	-2/+5
\| \| \| \| \| \| \| \| \|	with some static analysis tools). */PrintAsm.ml: don't cfa_adjust at Pfreeframe, as more code from the function can appear after (in case of tailcalls). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2256 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Remove some useless "Require".	xleroy	2012-12-30	1	-1/+0
\| \| \| \| \| \| \|	Update ARM port. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support for inlined built-ins.	xleroy	2010-06-29	1	-2/+2
\| \| \| \| \| \| \| \| \| \| \| \| \|	AST: add ef_inline flag to external functions. Selection: recognize calls to inlined built-ins and inline them as Sbuiltin. CminorSel to Asm: added Sbuiltin/Ibuiltin instruction. PrintAsm: adapted expansion of builtins. C2Clight: adapted detection of builtins. Conventions: refactored in a machine-independent part (backend/Conventions) and a machine-dependent part (ARCH/SYS/Conventions1). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Added tail call optimization pass	xleroy	2009-03-26	1	-0/+110
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1015 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e