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	-22/+9
\| \| \| \| \| \| \| \| \| \|	- 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	-0/+2
\| \| \| \|	clobber lists.
*	Take asm clobbers into account for determining callee-save registers used.	Xavier Leroy	2015-04-23	1	-0/+7
\|
*	Support for GCC-style extended asm, continued:	Xavier Leroy	2015-04-21	1	-2/+2
\| \| \| \| \| \| \| \|	- support "r", "m" and "i" constraints - support "%Q" and "%R" modifiers for register pairs - support register clobbers - split off analysis and transformation of asm statements in cparser/ExtendedAsm.ml
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20	1	-4/+4
\| \| \| \| \| \| \| \| \|	1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the reuse-temps branch:	xleroy	2010-09-02	1	-0/+40
	- Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e