compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge branch 'named-structs'	Xavier Leroy	2015-01-23	1	-1/+1
\|\ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Switch CompCert C / Clight AST of composite types (structs and unions) from a structural representation to a nominal representation, closer to concrete syntax. - This avoids algorithmic inefficiencies due to the structural representation. - Closes PR#4. - Smallstep: make small-step semantics more polymorphic in the type of the global environment. - Globalenvs: introduce Senv.t (symbol environments) as a restricted view on Genv.t (full global environments). - Events, Smallstep: use Senv instead of Genv to talk about global names.
\| *	Introduce symbol environments (type Senv.t) as a restricted view on global ↵	Xavier Leroy	2014-11-26	1	-1/+1
\| \| \| \| \| \| \| \|	environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
* \|	Follow-up to [5aecefe]: be conservative also in the case of a "common" ↵	Xavier Leroy	2015-01-20	1	-6/+21
\| \| \| \| \| \| \| \|	global const variable.
* \|	More prudent analysis of uninitialized const global variables.	Xavier Leroy	2015-01-09	1	-3/+6
\|/ \| \| \| \| \| \|	In the presence of separate compilation and linking, an uninitialized const global variable may be initialized elsewhere with a pointer value, falsifying the points-to analysis. Report and fix by Chung-Kil Hur and Jeehoon Kang.
*	Merge of "newspilling" branch:	xleroy	2014-07-23	1	-2/+2
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- 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
*	Add option -Os to optimize for code size rather than for execution speed.	xleroy	2014-02-19	1	-3/+4
\| \| \| \| \| \| \| \|	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
*	Updated ARM backend wrt new static analyses and optimizations.	xleroy	2014-01-02	1	-0/+12
\| \| \| \| \| \| \| \|	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
*	Ctypes.sizeof ty = 0 for empty types ty (zero-sized array, empty struct/union).	xleroy	2013-12-30	1	-3/+0
\| \| \| \| \| \| \|	__builtin_memcpy_aligned now supports the case sz = 0. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2392 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of branch value-analysis.	xleroy	2013-12-20	1	-0/+1812
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e