compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Long-overdue renaming: val_inject -> Val.inject, etc, for consistency with ↵	Xavier Leroy	2015-04-30	1	-17/+17
\| \| \| \|	Val.lessdef, etc.
*	Extend annotations so that they can keep track of global variables and local ↵	Xavier Leroy	2015-03-27	1	-0/+77
\| \| \| \| \| \| \| \| \| \|	variables whose address is taken. - CminorSel, RTL: add "annot" instructions. - CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions. - AST, Events: simplify EF_annot because constants are now part of the arguments. Implementation is not complete yet.
*	Introduce symbol environments (type Senv.t) as a restricted view on global ↵	Xavier Leroy	2014-11-26	1	-3/+3
\| \| \| \|	environments (type Genv.t). Use symbol environments instead of global environments for external functions (module Events).
*	Verification of the Unusedglob pass (removal of unreferenced static global ↵	Xavier Leroy	2014-11-24	1	-0/+1256
	definitions). Assorted changes to ia32/Op.v. PowerPC and ARM need updating.