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
*	Refactoring: move symbol_offset into Genv.	xleroy	2014-05-24
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Add option -Os to optimize for code size rather than for execution speed.	xleroy	2014-02-19
\| \| \| \| \| \| \| \|	Refactored compilation flags that affect the Coq part (module Compopts). Added support for C99 for loops with declarations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 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
*	Simplify LPMap by smashing bottoms.	xleroy	2013-08-12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2306 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Change interface of Kildall solvers to avoid precomputing the map pc -> list ↵	xleroy	2013-08-12
\| \| \| \| \| \|	of successors. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2305 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the "princeton" branch:	xleroy	2013-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 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
*	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
*	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
*	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
*	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
*	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
*	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
*	Merge of the newmem branch:	xleroy	2012-05-21
\| \| \| \| \| \| \| \| \| \|	- Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Added volatile_read_global and volatile_store_global builtins.	xleroy	2012-01-15
\| \| \| \| \| \| \|	Finished updating IA32 and ARM ports. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1792 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
*	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
*	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
*	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
*	Support for inlined built-ins.	xleroy	2010-06-29
\| \| \| \| \| \| \| \| \| \| \| \| \|	AST: add ef_inline flag to external functions. Selection: recognize calls to inlined built-ins and inline them as Sbuiltin. CminorSel to Asm: added Sbuiltin/Ibuiltin instruction. PrintAsm: adapted expansion of builtins. C2Clight: adapted detection of builtins. Conventions: refactored in a machine-independent part (backend/Conventions) and a machine-dependent part (ARCH/SYS/Conventions1). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 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
*	- Extended traces so that pointers within globals are supported as event values.	xleroy	2010-05-10
\| \| \| \| \| \| \| \|	- Revised handling of volatile reads: the execution environment dictates the value read, via the trace of events. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1345 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of the newmem and newextcalls branches:	xleroy	2010-03-07
\| \| \| \| \| \| \| \| \| \|	- Revised memory model with concrete representation of ints & floats, and per-byte access permissions - Revised Globalenvs implementation - Matching changes in all languages and proofs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Added support for jump tables in back end.	xleroy	2009-11-10
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1171 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	"val_match_approx_increasing" moved from mach-dep part to mach-indep part.	xleroy	2009-08-18
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1128 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Refactoring of Constprop and Constpropproof into a machine-dependent part ↵	xleroy	2009-08-17
\| \| \| \| \| \|	and a machine-independent part. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Reorganized the development, modularizing away machine-dependent parts.	xleroy	2008-12-30
\| \| \| \| \| \| \| \| \|	Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Ajout license, README, copyright notices	xleroy	2008-01-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fusion des modifications faites sur les branches "tailcalls" et "smallstep".	xleroy	2007-08-04
\| \| \| \| \| \| \| \| \| \| \| \|	En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revu traitement des variables globales dans AST.program et dans Globalenvs.	xleroy	2006-09-05
\| \| \| \| \| \| \| \|	Adaptation frontend, backend en consequence. Integration passe C -> C#minor dans common/Main.v. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@77 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fusion de la branche "traces":	xleroy	2006-09-04
\| \| \| \| \| \| \| \| \| \| \| \| \|	- Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Initial import of compcert	xleroy	2006-02-09
	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e