debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	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
*	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
*	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
*	Support compile-time constant expressions as arguments to gcc-style attributes	xleroy	2011-04-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1641 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Typos	xleroy	2011-04-19
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1640 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fixed some typos.	xleroy	2011-04-17
\| \| \| \| \| \| \|	Avoid generation of stubs for external functions without float arguments. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1639 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Use memcpy_word only if alignment AND size are multiples of word size.	xleroy	2011-04-17
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1638 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fixed some typos	xleroy	2011-04-16
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1637 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
*	Revised handling of GCC attributes. Preliminary, untested support for ↵	xleroy	2011-04-14
\| \| \| \| \| \|	__aligned__ attribute git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1634 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
*	Revised handling of sizeof(string-literal)	xleroy	2011-03-15
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Special case for while(1), for(..., 1, ...) and do ... while(0) loops.	xleroy	2011-03-15
\| \| \| \| \| \| \| \|	Don't wait until Constprop to get rid of trivial loop tests; instead, produces better-looking Cminor. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1610 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update for 1.8.1	xleroy	2011-03-14
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1609 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
*	Incompatibility 8.3 / 8.3pl1	xleroy	2011-03-14
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1606 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Comment char for Diab	xleroy	2011-03-13
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1605 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Slightly nicer semantics for initialization	xleroy	2011-03-13
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1604 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More global initialization work done and proved in Coq.	xleroy	2011-03-13
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1603 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Initializers for global variables: compile-time evaluation of expressions ↵	xleroy	2011-03-12
\| \| \| \| \| \|	done in Coq (module Initializers), using the same primitives as those for CompCert C's semantics. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1602 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Undesirable optimization of 'print'	xleroy	2011-03-10
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1601 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Bitfields: MSB-to-LSB in addition to LSB-to-MSB	xleroy	2011-03-10
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1600 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised signed/unsigned char handling.	xleroy	2011-03-10
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1599 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Improved test harness	xleroy	2011-03-10
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1598 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile.	xleroy	2011-03-09
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1597 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Treat "char" as unsigned OR signed depending on the configuration.	xleroy	2011-03-09
\| \| \| \| \| \| \|	Fixed infinite expansion of some recursive struct type where recursion goes through a typeded. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1596 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
*	In StructAssign: be careful not to duplicate accesses to a volatile variable.	xleroy	2010-11-10
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1551 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
*	Various algorithmic improvements that reduce compile times (thanks Alexandre ↵	xleroy	2010-10-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Pilkiewicz): - Lattice: preserve sharing in "combine" operation - Kildall: use splay heaps (lib/Heaps.v) for node sets - RTLgen: add a "nop" before loops so that natural enumeration of nodes coincides with (reverse) postorder - Maps: add PTree.map1 operation, use it in RTL and LTL. - Driver: increase minor heap size git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1543 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	License for Floataux.ml	xleroy	2010-10-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1542 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Inconsistent treatment of "lone" zero-width bit fields	xleroy	2010-09-24
\| \| \| \| \| \| \|	(i.e. not preceded by another bit field). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1516 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Bizarre use of struct value	xleroy	2010-09-21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1513 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
*	Typo in doc comment	xleroy	2010-09-21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1511 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Memory.v: added drop_perm operation	xleroy	2010-09-21
\| \| \| \| \| \| \| \|	Globalenvs.v: used drop_perm to set appropriate permissions on global variables (Notempty if volatile; Readable if readonly; Writable otherwise) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1510 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	No crash if nonexistent input file.	xleroy	2010-09-14
\| \| \| \| \| \| \|	Heuristic to choose test data. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1509 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
*	Updated	xleroy	2010-09-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1505 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	++ on volatile not supported.	xleroy	2010-09-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1504 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
*	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
*	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
*	Better emulation of long long as a struct.	xleroy	2010-09-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1500 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