debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	Merge of the nonstrict-ops branch:	xleroy	2012-01-14
\| \| \| \| \| \| \| \| \| \| \|	- Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml chars	xleroy	2011-10-18
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised emulation of packed structs	xleroy	2011-10-16
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1729 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Watch out for min_int / -1	xleroy	2011-08-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1727 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Cleaned up old commented-out parts	xleroy	2011-08-19
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More careful treatment of 'load immediate 0' as 'xor self'	xleroy	2011-08-18
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1718 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Forgot to update: adding xchg instruction	xleroy	2011-08-16
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1712 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Locations.v: add Loc.diff_dec.	xleroy	2011-08-14
\| \| \| \| \| \| \| \|	ia32: lift restriction that 1st arg of ops cannot be ECX (could be useful for a future, better reloading strategy) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1711 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	IA32 PrintAsm.ml: wrong moves generated in print_builtin_memcpy_big	xleroy	2011-08-10
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1706 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	IA32 port: more faithful treatment of pseudoregister ST0.	xleroy	2011-08-08
\| \| \| \| \| \| \|	Related general change: support for destroyed_at_moves. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1700 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Cleaned up handling of composite conditions	xleroy	2011-08-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1699 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
*	Added animation of the CompCert C semantics (ccomp -interp)	xleroy	2011-07-28
\| \| \| \| \| \| \| \|	test/regression: int main() so that interpretation works Revised once more implementation of __builtin_memcpy (to check for PPC & ARM) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1688 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
*	Nicer printing of annotations.	xleroy	2011-05-23
\| \| \| \| \| \| \|	ia32: support builtins for reversed reads and writes (facilitates testing). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1655 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	cparser/StructAssign: always use __builtin_memcpy + alignment indication	xleroy	2011-05-11
\| \| \| \| \| \| \| \| \| \|	(simpler and globally more efficient) cfrontend/C2C.ml: specialization of __builtin_memcpy over size /PrintAsm.ml: revised expansion of __builtin_memcpy_ ia32/Asm.ml: typo in comment git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1649 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Added pass CleanupLabels to remove unreferenced labels in a proved way.	xleroy	2011-05-08
\| \| \| \| \| \| \| \| \| \|	ia32/PrintAsm.ml: simplified accordingly; other PrintAsm.ml to be fixed. ia32/Asm.v: Pmov_ri can undef flags (if translated to xor) cparser/Ceval.ml: treat ~ in constant exprs git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	cparser/Elab: __attribute, not attribute	xleroy	2011-04-16
\| \| \| \| \| \| \| \|	ia32/PrintAsm: wrong section name regression: added test attribs1 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1636 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Preliminary support for 'aligned' and 'section' attributes, gcc-style. ↵	xleroy	2011-04-16
\| \| \| \| \| \|	New-style handling of sections for IA32 and ARM. Work in progress, to be tested. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1635 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Renamed Machconcr into Machsem.	xleroy	2011-04-09
\| \| \| \| \| \| \| \|	Removed Machabstr and Machabstr2concr, now useless following the reengineering of Stacking. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1633 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of branch "unsigned-offsets":	xleroy	2011-04-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- In pointer values "Vptr b ofs", interpret "ofs" as an unsigned int. (Fixes issue with wrong comparison of pointers across 0x8000_0000) - Revised Stacking pass to not use negative SP offsets. - Add pointer validity checks to Cminor ... Mach to support the use of memory injections in Stacking. - Cleaned up Stacklayout modules. - IA32: improved code generation for Mgetparam. - ARM: improved code generation for op-immediate instructions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1632 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Use movapd instead of movsd for xmm reg-reg move: it avoids partial register ↵	xleroy	2010-11-28
\| \| \| \| \| \|	stalls, resulting in tiny speedups. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1556 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	float->int conversions, continued: weaker axiomatization.	xleroy	2010-10-29
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1545 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Float.intoffloat and Float.intuoffloat are now partial functions.	xleroy	2010-10-28
\| \| \| \| \| \| \|	(May fail if float is too big to be converted.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1544 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Comments	xleroy	2010-09-10
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1508 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Improvements for int8 and int16 stores	xleroy	2010-09-10
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1507 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updates for IA32-Cygwin.	xleroy	2010-09-08
\| \| \| \| \| \| \| \|	cparser/Elab.ml: tolerate changes in qualifiers in ?: cfrontend/C2C.ml: revise info attached to atoms; treat inline functions as static. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1506 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update: adding __builtin_annotation	xleroy	2010-09-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support for __builtin_fmax and __builtin_fmin	xleroy	2010-09-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1501 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the reuse-temps branch:	xleroy	2010-09-02
	- Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e