compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Extended inline asm: revised treatment of clobbered registers.	Xavier Leroy	2015-05-09	1	-1/+0
\| \| \| \| \| \| \| \| \| \|	- Treat clobbered registers as being destroyed by EF_inline_asm builtins (which is the truth, semantically). - To enable the above, represent clobbers as Coq strings rather than idents and move register_by_name from Machregsaux.ml to Machregs.v. - Side benefit: more efficient implementation of Machregsaux.name_of_register. -# Please enter the commit message for your changes. Lines starting
*	Allow "scratch" (non-allocatable temporary registers) to be mentioned in asm ↵	Xavier Leroy	2015-04-23	1	-1/+2
\| \| \| \|	clobber lists.
*	Take asm clobbers into account for determining callee-save registers used.	Xavier Leroy	2015-04-23	1	-0/+1
\|
*	Pretty-printers for RTL and LTL. Not yet well integrated.	xleroy	2010-05-02	1	-0/+1
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1332 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Coloring: allow to exclude user-specified registers from allocation.	xleroy	2010-04-10	1	-0/+16
	CPragmas (PPC/EABI only): add #pragma reserve_register git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1314 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e