compcert - CompCert fork with minor modifications for Vericert.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Updated PR by removing whitespaces. Bug 17450.	Bernhard Schommer	2015-10-20	1	-5/+5
\|
*	Simplify the handling of extended inline asm, taking advantage of the new, ↵	Xavier Leroy	2015-08-21	1	-6/+5
\| \| \| \|	structured builtin arguments and results.
*	Extended inline asm: revised treatment of clobbered registers.	Xavier Leroy	2015-05-09	1	-3/+4
\| \| \| \| \| \| \| \| \| \|	- 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/+1
\| \| \| \|	clobber lists.
*	Extended asm: more lenient treatment of constraints.	Xavier Leroy	2015-04-22	1	-10/+21
\| \| \| \| \|	We can ignore alternatives as long as one of the constraints we handle (r, m, i, n) is there.
*	Avoid multiple errors being reported in the case #outputs >= 2.	Xavier Leroy	2015-04-21	1	-2/+6
\|
*	Support for GCC-style extended asm, continued:	Xavier Leroy	2015-04-21	1	-0/+183
	- 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