debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	configure: distinguish between ABI and processor model.	xleroy	2014-07-29
\| \| \| \| \| \| \| \|	ARM: various tweaks, incl. support for SDIV and UDIV insns when available. test/regression/funptr2.c: Thumb does weird things with <function ptr>+1. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	ARM port: add support for Thumb2. To be tested.	xleroy	2014-07-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2549 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Adapt to the two different calling conventions for floats.	xleroy	2014-05-02
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2476 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	stdarg.h: assorted fixes for PowerPC	xleroy	2014-01-01
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2397 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fine hair splitting depending on whether va_list is a scalar type (IA32, ↵	xleroy	2014-01-01
\| \| \| \| \| \|	ARM) or an array type (PowerPC). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2395 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Experimental support for <stdarg.h>, the GCC way. Works on IA32. To be ↵	xleroy	2014-01-01
\| \| \| \| \| \|	tested on PowerPC and ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	powerpc: faster implementation of long division modeled on that for IA32	xleroy	2013-07-03
\| \| \| \| \| \| \| \|	test: add one test (2^64-1) / (2^32+3) to exercise a special case of this long division. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2288 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the "princeton" branch:	xleroy	2013-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fix compilation of runtime system.	xleroy	2013-05-29
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2263 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Syntax errors	xleroy	2013-05-06
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2237 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Wrong pseudo-instr	xleroy	2013-05-06
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2236 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support for in64 -> float conversions w/ correct rounding.	xleroy	2013-05-06
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2235 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	ia32/i64_dtou: wrong play on rounding mode	xleroy	2013-05-05
\| \| \| \| \| \| \| \| \|	arm, powerpc: expand shifts inline in dtos and dtou arm: branchless code for shl and shr test: more tests for double -> long long conversions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2234 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Typos in comments	xleroy	2013-04-30
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2220 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Expand 64-bit integer comparisons into 32-bit integer comparisons.	xleroy	2013-04-29
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Missing GLOB	xleroy	2013-04-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2215 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Make ia32/ code more portable across systems.	xleroy	2013-04-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2214 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fixes in PowerPC port	xleroy	2013-04-21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2209 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Split arch/int64.s into one file per function.	xleroy	2013-04-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2206 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Configuring the assembler used for the runtime lib	xleroy	2013-04-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2205 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Remove __i64_{neg,add,sub,mul}, now handled directly by the compiler.	xleroy	2013-04-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2204 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
*	Support for indirect symbols under MacOS X (final).	xleroy	2012-07-14
\| \| \| \| \| \| \|	Remove stdio hack in runtime/ git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1979 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Simplified stdlib wrapper; use it only under MacOS X	xleroy	2010-09-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the newmem and newextcalls branches:	xleroy	2010-03-07
\| \| \| \| \| \| \| \| \| \|	- Revised memory model with concrete representation of ints & floats, and per-byte access permissions - Revised Globalenvs implementation - Matching changes in all languages and proofs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Some cleanups	xleroy	2009-01-02
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@937 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Removed vfprintf, because it was causing portability problems	xleroy	2008-12-31
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@931 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Compilo C, preprocesseur, assembleur sont determines par configure et mis ↵	xleroy	2008-04-19
\| \| \| \| \| \|	dans Makefile.config git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout license, README, copyright notices	xleroy	2008-01-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefiles	xleroy	2007-08-06
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fusion des modifications faites sur les branches "tailcalls" et "smallstep".	xleroy	2007-08-04
	En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e