compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Track the locations of local variables using EF_debug annotations.	Xavier Leroy	2015-08-23	1	-0/+3
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	SimplLocals: - record locations of stack-allocated variables with annotations (of kind 5) at the beginning of the function; - mark every assignment to non-stack-allocated variables with an annotation of kind 2. Debugvar: (new pass!) - perform availability analysis for debug annotations of kind 2 - insert "start of live range" and "end of live range" annotations (kind 3 and 4) to delimit intervals of PCs where the location of a local variable is known.
*	Add flags to control individual optimization passes + flag -O0 for turning ↵	Xavier Leroy	2014-11-16	1	-1/+10
\| \| \| \|	them off.
*	ARM port: add support for Thumb2. To be tested.	xleroy	2014-07-27	1	-1/+2
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2549 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Add option -Os to optimize for code size rather than for execution speed.	xleroy	2014-02-19	1	-0/+33
	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