debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	Merge of "newspilling" branch:	xleroy	2014-07-23
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	ia32/Select*: complete the modifications to shifts.	xleroy	2014-04-11
\| \| \| \| \| \| \| \| \|	Makefile: missing "clean" actions. Makefile/pg/coq: honor $COQBIN if set (as suggested by P. Boutillier) to facilitate testing with different Coq versions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2453 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons ↵	xleroy	2014-04-09
\| \| \| \| \| \| \| \| \| \|	over booleans. Select*: more systematic constant propagation; don't CP shifts by amounts outside of [0..31]. Driver: timer for whole compilation. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support Onot operator / notl instruction. More constant propagation during ↵	xleroy	2014-04-06
\| \| \| \| \| \|	selection. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2451 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Force dependency of SelectOp on Compopts.	xleroy	2014-03-03
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2428 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of branch value-analysis.	xleroy	2013-12-20
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2381 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms	xleroy	2013-09-14
\| \| \| \| \| \| \| \| \|	are necessary, only two parameters (default_pl and choose_binop_pl). SelectDiv: optimize FP division by a power of 2. ConstpropOp: optimize 2.0 * x and x * 2.0 into x + x. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2326 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Optimize integer divisions by positive constants, turning them into	xleroy	2013-07-29
\| \| \| \| \| \| \|	multiply-high and shifts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 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
*	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
*	Remove some useless "Require".	xleroy	2012-12-30
\| \| \| \| \| \| \|	Update ARM port. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2085 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
*	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
*	Support for MacOS X's indirect symbols. (first try)	xleroy	2012-07-13
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1978 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Take advantage of Cmaskzero and Cmasknotzero.	xleroy	2012-02-24
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1825 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the "volatile" branch:	xleroy	2012-02-04
\| \| \| \| \| \| \| \| \| \| \| \|	- native treatment of volatile accesses in CompCert C's semantics - translation of volatile accesses to built-ins in SimplExpr - native treatment of struct assignment and passing struct parameter by value - only passing struct result by value remains emulated - in cparser, remove emulations that are no longer used - added C99's type _Bool and used it to express \|\| and && more efficiently. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1814 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	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