debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	Follow-up to commit 2613	xleroy	2014-08-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2614 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	PowerPC port: refactored the expansion of built-in functions and	xleroy	2014-07-28
\| \| \| \| \| \| \| \| \| \|	pseudo-instructions so that it does not need to be re-done in cchecklink. cchecklink: updated accordingly. testsuite: compile with -sdump and run cchecklink if supported. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2553 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update for single-precision floats. Calls to vararg functions remain	xleroy	2014-07-24
\| \| \| \| \| \| \|	to be updated. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2544 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Future-proofing: keep signature information in IA32 and PowerPC Asm, just ↵	xleroy	2013-12-26
\| \| \| \| \| \|	like we already do in ARM Asm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2385 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	powerpc/: new unary operation "addsymbol"	xleroy	2013-11-17
\| \| \| \| \| \| \| \|	Support far-data addressing in sections. (Currently ignored in checklink.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2368 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update cchecklink w/ new Asm instructions Pmulh*	xleroy	2013-07-29
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2301 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated to Pbuiltin with list of results	xleroy	2013-04-30
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2222 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Big merge of the newregalloc-int64 branch. Lots of changes in two directions:	xleroy	2013-04-20
\| \| \| \| \| \| \| \| \|	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
*	Ported to Coq 8.4pl1. Merge of branches/coq-8.4.	xleroy	2013-01-29
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revert unintentional commit #1955	xleroy	2012-07-06
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1957 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout trunk CompCert	blazy	2012-07-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1955 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: adaptation to the new floats	varobert	2012-07-03
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1949 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Tracing each data chunk in debug mode	varobert	2012-04-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1873 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink: first import of Valentin Robert's validator for asm and link	xleroy	2012-03-28
	cparser: renamed Errors to Cerrors; removed packing into Cparser. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1856 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e