debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
...
*	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
*	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
*	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
*	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
*	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
*	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
*	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
*	Renamed C2Clight into C2C	xleroy	2010-08-18
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1468 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge of branches/full-expr-4:	xleroy	2010-08-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Csyntax, Csem: source C language has side-effects within expressions, performs implicit casts, and has nondeterministic reduction semantics for expressions - Cstrategy: deterministic red. sem. for the above - Clight: the previous source C language, with pure expressions. Added: temporary variables + implicit casts. - New pass SimplExpr to pull side-effects out of expressions (previously done in untrusted Caml code in cparser/) - Csharpminor: added temporary variables to match Clight. - Cminorgen: adapted, removed cast optimization (moved to back-end) - CastOptim: RTL-level optimization of casts - cparser: transformations Bitfields, StructByValue and StructAssign now work on non-simplified expressions - Added pretty-printers for several intermediate languages, and matching -dxxx command-line flags. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1467 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
*	Merging the Princeton implementation of the memory model. Separate axioms ↵	xleroy	2010-06-28
\| \| \| \| \| \|	in file lib/Axioms.v. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1354 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
*	Cleaned up handling of linker sections.	xleroy	2010-05-08
\| \| \| \| \| \| \|	Minor updates on ARM code generator. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1339 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Options -I -D -U with a space	xleroy	2010-03-30
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1302 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Handling of volatile accesses through builtin functions.	xleroy	2010-03-08
\| \| \| \| \| \| \| \| \|	Added support for processor-specific builtin functions. Added some PowerPC instructions as builtins. Updated #pragma section handling. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1285 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Handling of builtins, continued.	xleroy	2010-03-07
\| \| \| \| \| \| \|	PrintCsyntax, PrintAsm: improve printing of float literals. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1284 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
*	Suppressed -fall-extensions option, too dangerous wrt flonglong	xleroy	2010-03-03
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1275 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Switching to the new C parser/elaborator/simplifier	xleroy	2010-03-03
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Revised handling of #pragma section and small data areas	xleroy	2010-01-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1235 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	PowerPC/EABI port: preliminary support for #pragma section and	xleroy	2009-11-03
\| \| \| \| \| \| \| \| \| \|	#pragma use_section. Some clean-ups in Cil2Csyntax. Separate mach-dep parts of extraction/extraction.v into <arch>/extractionMachdep.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1167 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Simplified the treatment of the PowerPC small data area; now more specific ↵	xleroy	2009-11-02
\| \| \| \| \| \|	to the Diab toolchain. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1165 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Preliminary support for small data area in PowerPC port.	xleroy	2009-11-01
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1163 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	No '\n' in Coq strings...	xleroy	2009-08-18
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Distinguish two kinds of nonterminating behaviors: silent divergence	xleroy	2009-08-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	and reactive divergence. As a consequence: - Removed the Enilinf constructor from traceinf (values of traceinf type are always infinite traces). - Traces are now uniquely defined. - Adapted proofs big step -> small step for Clight and Cminor accordingly. - Strengthened results in driver/Complements accordingly. - Added common/Determinism to collect generic results about deterministic semantics. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1123 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Added 'going wrong' behaviors	xleroy	2009-08-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1120 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Adapted to work with Coq 8.2-1	xleroy	2009-06-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1076 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Added tail call optimization pass	xleroy	2009-03-26
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1015 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	- Added alignment constraints to memory loads and stores.	xleroy	2009-01-11
\| \| \| \| \| \| \| \| \| \| \|	- In Cminor and below, removed pointer validity check in semantics of comparisons, so that evaluation of expressions is independent of memory state. - In Cminor and below, removed "alloc" instruction. - Cleaned up commented-away parts. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 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