debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
*	PowerPC: remove the fmadd and fmsub operators/Asm instructions	xleroy	2012-03-07
\| \| \| \| \| \| \| \|	(definitely not semantics-preserving; hard to justify). CPragmas: make sure SDAs are not recognized on MacOSX. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1836 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Make CPragmas common to all ports.	xleroy	2012-02-27
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1828 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
*	Improved instruction selection for "notint".	xleroy	2012-02-24
\| \| \| \| \| \| \|	powerpc/PrintAsm.ml: fixed MacOS X problems with malloc and free git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1824 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	More aggressive common subexpression elimination (CSE) of memory loads.	xleroy	2012-02-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1823 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Simplified and cleaned up the passing of information from C2C to PrintAsm, ↵	xleroy	2012-02-22
\| \| \| \| \| \|	as well as the handling of sections. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1822 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Work around limited excursion of conditional branches	xleroy	2012-02-13
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1817 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
*	Another typo in print_builtin_vstore_common	xleroy	2012-01-21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1801 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Typo in print_builtin_vstore_common	xleroy	2012-01-21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1800 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	powerpc/SelectOp: optimize the pattern ((x >>s N) & N1) & N2 common in a ↵	xleroy	2012-01-21
\| \| \| \| \| \| \| \| \|	certain customer's code backend/Coloringaux: avoid spilling the dummy result registers for built-ins that have no result. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1799 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Cosmetic cleanups.	xleroy	2012-01-15
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1793 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
*	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
*	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
*	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
*	More builtins for ARM and PowerPC	xleroy	2011-08-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1697 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated Makefile and dependencies. Typo in powerpc/PrintAsm.ml.	xleroy	2011-07-28
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1689 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
*	Back from Oregon commit.	xleroy	2011-07-05
\| \| \| \| \| \| \| \| \|	powerpc/: better compilation of some comparisons; revised asmgenproof1. common/: added Mem.storebytes; used to give semantics to memcpy builtin. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1679 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Forgot to print Oroli op	xleroy	2011-06-22
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1677 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Recognition of rlwimi instruction (useful for bitfield assignment)	xleroy	2011-06-21
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1676 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
*	Oaddrsymbol and small data area	xleroy	2011-06-07
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1667 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: support for attributes over struct and union.	xleroy	2011-05-12
\| \| \| \| \| \| \| \|	cparser: added experimental emulation of packed structs (PackedStruct.ml) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1650 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
*	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
*	Fixed some typos	xleroy	2011-04-16
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1637 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
*	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
*	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
*	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
*	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
*	Adding __builtin_annotation	xleroy	2010-09-01
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext	xleroy	2010-08-21
\| \| \| \| \| \| \| \| \|	as bitwise operations rather than arithmetic ones. CastOptimproof: fixed for ARM port. Other files: adapted to changes in Integers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1472 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
*	Fix extraction problem	xleroy	2010-07-14
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1418 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
*	Updated Caml parts to match new representation for global variables.	xleroy	2010-05-26
\| \| \| \| \| \| \|	*/PrintAsm.ml: watch out for large stack frames in Pallocframe. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1349 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