debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	debian/changelog: Tag 2.4-1 for unstable releaseHEAD master	Benjamin Barenblat	2015-02-05
\|
*	Don’t reference a nonexistent upstream LICENSE file	Benjamin Barenblat	2015-02-05
\| \| \| \|	Use the Debian copyright file instead.
*	Add Vcs-Browser and Vcs-Git URLs	Benjamin Barenblat	2015-02-05
\|
*	Add man page	Benjamin Barenblat	2015-02-05
\|
*	Install CompCert README	Benjamin Barenblat	2015-02-05
\|
*	debian/rules: Better documentation	Benjamin Barenblat	2015-02-05
\|
*	Install manually	Benjamin Barenblat	2015-02-05
\| \| \| \| \|	The CompCert installation target is fairly inflexible, and it’s inadequate for packaging. Install everything manually instead.
*	Pass target to configure	Benjamin Barenblat	2015-02-05
\| \| \| \| \| \| \|	The CompCert configure script isn’t a standard configure script: It takes a positional argument specifying the architecture it should target. Override dh_auto_configure to do nothing, and pass the relevant arguments to configure in dh_auto_build.
*	Fix minor error in Debian copyright file	Benjamin Barenblat	2015-02-05
\|
*	Fake a Makefile.config so initial ‘make clean’ works	Benjamin Barenblat	2015-02-05
\| \| \| \| \|	The Makefile requires a Makefile.config to run anything, so create an empty Makefile.config before starting to run make commands.
*	Begin packaging CompCert	Benjamin Barenblat	2015-02-05
\|
*	Merge tag 'upstream/2.4'	Benjamin Barenblat	2015-02-05
\|\ \| \| \| \| \| \|	Upstream version 2.4
\| *	Imported Upstream version 2.4upstream/2.4 upstream	Benjamin Barenblat	2015-02-05
\|/
*	Trim blank lines	xleroy	2014-09-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2625 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update changelog and version for 2.4	xleroy	2014-09-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2624 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Tolerance in parsing of 'section' pragma	xleroy	2014-09-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2623 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Cold feet: suppress builtins for load with reservation/store conditional, ↵	xleroy	2014-08-28
\| \| \| \| \| \|	use case is unclear. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update	xleroy	2014-08-28
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2621 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update for 2.4	xleroy	2014-08-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2620 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Rename __builtin_cntlz to __builtin_clz.	xleroy	2014-08-27
\| \| \| \| \| \| \|	IA32: add __builtin_clz, __builtin_ctz. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More efficient implementations of map, fold, etc.	xleroy	2014-08-27
\| \| \| \| \| \| \|	(Contributed by Vincent Laporte.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2618 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More careful detection of inlined builtins. Produces better error messages ↵	xleroy	2014-08-25
\| \| \| \| \| \|	if an unsupported __builtin_xxx function is used by mistake. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2617 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Use VFD regs to implement 64-bit mem-mem copies in builtin_memcpy_false.	xleroy	2014-08-21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2616 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support C99 compound literals (by expansion in Unblock pass).	xleroy	2014-08-21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	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
*	Add builtins for load with reservation and conditional store.	xleroy	2014-08-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2613 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Wrong types for strex builtins.	xleroy	2014-08-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2612 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Better validation of target for ARM	xleroy	2014-08-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Obvious typos in commit r2609	xleroy	2014-08-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2610 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Add some more synchronization builtins	xleroy	2014-08-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2609 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Improve error reporting for unsupported compound literals.	xleroy	2014-08-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2608 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Excessively strict validation: ofs + sz < modulus should have been	xleroy	2014-08-20
\| \| \| \| \| \| \|	ofs + sz <= modulus. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2607 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Rename "-fthumb" option into "-mthumb" for GCC compatibility.	xleroy	2014-08-19
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2572 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	checklink/Check.ml: missing SDA addressing for store instructions.	xleroy	2014-08-19
\| \| \| \| \| \| \| \|	powerpc/PrintAsm.ml: update Linux output (Csymbol_rel, SDA sections). test/regression/sections.c: test for SDA and relative addressings. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2571 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update dependencies	xleroy	2014-08-19
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2570 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.	xleroy	2014-08-18
\| \| \| \| \| \| \| \| \| \| \|	powerpc/Asmgen*: simplify the code generated for far-data relative accesses, so that the only occurrences of Csymbol_rel_{low,high} are in the pattern Paddis(r, GPR0, Csymbol_rel_high...); Paddi(r, r, Csymbol_rel_low...) checklink/Check.ml: check the pattern above. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2569 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Improve error detection and error messages for enums.	xleroy	2014-08-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2568 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Issue with switch labels that are negative 32-bit integers.	xleroy	2014-08-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Add some tests for "switch" over 32 and 64-bit integers.	xleroy	2014-08-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2566 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	- Support "switch" statements over 64-bit integers	xleroy	2014-08-17
\| \| \| \| \| \| \| \| \| \| \| \| \|	(in CompCert C to Cminor, included) - Translation of "switch" to decision trees or jumptables made generic over the sizes of integers and moved to the Cminor->CminorSel pass instead of CminorSel->RTL as before. - CminorSel: add "exitexpr" to support the above. - ValueDomain: more precise analysis of comparisons against an integer literal. E.g. "x >=u 0" is always true. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2565 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Nicer reporting of I/O errors (e.g. "No such file").	xleroy	2014-08-13
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2564 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Spurious error on a local static function declaration	xleroy	2014-08-13
\| \| \| \| \| \| \|	("static int f(void);" inside a function). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2563 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update comment	xleroy	2014-08-13
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2562 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Add Mem.free_parallel_inject and use it to simplify Events a bit.	xleroy	2014-07-31
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2556 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	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
*	All targets: add __builtin_membar	xleroy	2014-07-28
\| \| \| \| \| \| \|	ARM: add __builtin_dsb __builtin_isb git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2554 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
*	Updated Changelog	xleroy	2014-07-28
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2552 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.	xleroy	2014-07-28
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2550 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