debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	Watch out for behaviors exponential in the nesting of struct/union types.	xleroy	2013-03-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2158 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More aggressive CSE across Ibuiltin.	xleroy	2013-03-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2152 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Assorted changes to reduce stack and heap requirements when compiling very ↵	xleroy	2013-03-16
\| \| \| \| \| \|	big functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2151 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More updates for 1.13	xleroy	2013-03-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2145 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated for version 1.13	xleroy	2013-03-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2143 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Glasnost: making transparent a number of definitions that were opaque	xleroy	2013-03-10
\| \| \| \| \| \| \| \|	for no good reason. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2140 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Finished backtracking (cf previous commit) for ARM and PowerPC.	xleroy	2013-03-04
\| \| \| \| \| \| \|	ARM: slightly shorter code generated for indirect memory accesses. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2137 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Partial backtracking on previous commit: the "hole in Mach stack frame"	xleroy	2013-03-03
\| \| \| \| \| \| \| \|	trick prevents a future mapping of the Mach/Asm call stack as a single block. IA32 is fixed, PowerPC and ARM remains to be done. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2136 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised Stacking and Asmgen passes and Mach semantics:	xleroy	2013-03-01
\| \| \| \| \| \| \| \| \| \|	- no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Constant propagation within __builtin_annot.	xleroy	2013-02-24
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Pointers one past	xleroy	2013-02-15
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2118 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	lib/Integers.v: revised and extended, faster implementation based on	xleroy	2013-02-10
\| \| \| \| \| \| \| \|	bit-level operations provided by ZArith in Coq 8.4. Other modules: adapted accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2110 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
*	Update for release 1.12	xleroy	2013-01-09
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2097 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support for inline assembly (asm statements).	xleroy	2012-12-18
\| \| \| \| \| \| \|	cparser: add primitive support for enum types. bitfield emulation: for bitfields with enum type, choose signed/unsigned as appropriate git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2074 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Globalenvs: allocate one-byte block with permissions Nonempty for each	xleroy	2012-11-12
\| \| \| \| \| \| \| \| \| \| \|	function definition, so that comparisons between function pointers are correctly defined. AST, Globalenvs, and many other files: represent programs as a list of (function or variable) definitions instead of two lists, one for functions and the other for variables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2067 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Flocq-based parsing of floating-point literals (Jacques-Henri Jourdan)	xleroy	2012-11-03
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2065 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Generate output files in current directory; can be overriden with -o option	xleroy	2012-10-08
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2061 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of branch seq-and-or. See Changelog for details.	xleroy	2012-10-06
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2059 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More aggressive elimination of conditional branches during constant	xleroy	2012-08-01
\| \| \| \| \| \| \| \| \|	propagation, taking better advantage of inferred constants. Helps with the compilation of && and \|\| operators. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1987 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
*	Preparation for release 1.11	xleroy	2012-07-13
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1975 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Added option -falign-functions	xleroy	2012-07-01
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Changelog: updated	xleroy	2012-06-28
\| \| \| \| \| \| \| \| \| \|	driver/Interp.ml: clean up dead code lib/Integers.v: add shifted_or_is_add lib/Floats.v: add from_words_eq .depend: updated git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1940 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Make min_int / -1 and min_int % -1 semantically undefined	xleroy	2012-06-09
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1919 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	MAJ doc	xleroy	2012-03-12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1850 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of Andrew Tolmach's HASP-related changes	xleroy	2012-03-09
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1838 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	PowerPC: remove the fmadd and fmsub operators/Asm instructions	xleroy	2012-03-07
\| \| \| \| \| \| \| \|	(definitely not semantics-preserving; hard to justify). CPragmas: make sure SDAs are not recognized on MacOSX. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1836 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Added command-line options -Wp,<opt> -Wa,<opt> -Wl,<opt>	xleroy	2012-02-29
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1832 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	- Support for _Alignof(ty) operator from ISO C 2011	xleroy	2012-02-26
\| \| \| \| \| \| \| \| \| \|	and __alignof__(ty), __alignof__(expr) from GCC. - Resurrected __builtin_memcpy_aligned, useful for files generated by Scade KCG 6. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1827 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Translate CompCert C's "a ? b : c" to the equivalent simple Clight expr if	xleroy	2012-02-25
\| \| \| \| \| \| \|	b and c are simple. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1826 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More aggressive common subexpression elimination (CSE) of memory loads.	xleroy	2012-02-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1823 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Simplified and cleaned up the passing of information from C2C to PrintAsm, ↵	xleroy	2012-02-22
\| \| \| \| \| \|	as well as the handling of sections. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1822 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update	xleroy	2011-11-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1742 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Changelog, doc: updated for release 1.9	xleroy	2011-08-22
\| \| \| \| \| \| \|	lib/Integers, Makefile: unsuccessful experiments with coqchk git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1723 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Presimplification SimplVolatile: cleaned up and integrated.	xleroy	2011-08-18
\| \| \| \| \| \|	test/*/Makefile: normalized 'bench' target git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1717 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	MAJ	xleroy	2011-08-16
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1714 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	ARM: added reversed load/store builtins + bswap builtin (to be tested)	xleroy	2011-07-30
\| \| \| \| \| \| \| \|	IA32: added bswap builtin Updated Changelog git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1693 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	In conditional expressions e1 ? e2 : e3, cast the results of e2 and e3 to ↵	xleroy	2011-07-16
\| \| \| \| \| \| \| \| \|	the type of the whole conditional expression. Replaced predicates "cast", "is_true" and "is_false" by functions "sem_cast" and "bool_val". git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1684 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of branch new-semantics: revised and strengthened top-level statements ↵	xleroy	2011-07-15
\| \| \| \| \| \|	of semantic preservation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1683 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised handling of annotation statements, and more generally built-in ↵	xleroy	2011-06-13
\| \| \| \| \| \|	functions, and more generally external functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Forgot something	xleroy	2011-05-24
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1658 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update for release 1.8.2	xleroy	2011-05-24
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1656 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	cparser: support for attributes over struct and union.	xleroy	2011-05-12
\| \| \| \| \| \| \| \|	cparser: added experimental emulation of packed structs (PackedStruct.ml) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1650 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	powerpc/PrintAsm.ml arm/PrintAsm.ml: updated (no label elimination).	xleroy	2011-05-08
\| \| \| \| \| \| \| \| \| \|	Added -dmach option and corresponding printer for Mach code. CleanupLabelsproof.v: fixed for ARM Driver.ml: -E sends output to stdout; support for .s and .S source files. cparser/Elab.ml: spurious comment deleted. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1648 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update for 1.8.1 release	xleroy	2011-03-14
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1607 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update for release 1.8	xleroy	2010-09-21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1512 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated	xleroy	2010-09-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1505 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More faithful semantics for volatile reads and writes.	xleroy	2010-05-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update	xleroy	2010-05-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1336 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e