debian-compcert - Debian packaging for CompCert

	Commit message (Collapse)	Author	Age
...
*	Update for single-precision floats. Calls to vararg functions remain	xleroy	2014-07-24
\| \| \| \| \| \| \|	to be updated. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2544 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Add _a memory accesses.	xleroy	2014-07-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2543 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update with _a memory accesses	xleroy	2014-07-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2542 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Simplify COQINCLUDES	xleroy	2014-07-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2541 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Merge the various $(ARCH)/$(VARIANT)/xxx.v files into $(ARCH)/xxx.v.	xleroy	2014-07-23
\| \| \| \| \| \| \| \| \|	The only platform where we have two variants is ARM, and it's easier to share the callling convention code between the two than to maintain both variants separately. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2540 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Redundant -I in CAMLINCLUDES	xleroy	2014-07-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2539 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update "read_as_zeros" property.	xleroy	2014-07-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2538 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	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
*	Tweaks to support defunctorization.	xleroy	2014-07-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2536 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Make Alphabet.v compatible with an environnment where Containers is installed	jjourdan	2014-07-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2521 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Add Proof keyword so that documentation generation works	jjourdan	2014-07-04
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2520 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Add "read_as_zero" property for memory areas initialized by Init_space.	xleroy	2014-06-30
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2519 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Document commit r2507.	xleroy	2014-06-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2508 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Cleaner, more resilient parsing of pragmas.	xleroy	2014-06-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2507 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Instead of having two expansions of shrximm (one in SelectOp, one in ↵	xleroy	2014-05-28
\| \| \| \| \| \|	Asmgen), move the most efficient expansion to Asmgen. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2504 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
*	Empty declarations	jjourdan	2014-05-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	In enter_or_refine_ident: revised handling of "extern" decls.	xleroy	2014-05-18
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Another corner case for string literal initializers: char * x[] = { "lit" }	xleroy	2014-05-18
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2498 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Typo in struct_declaration_list causing conflicts.	xleroy	2014-05-18
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Bump	xleroy	2014-05-15
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2494 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	- Re-added support for "__func__" identifier as per ISO C99.	xleroy	2014-05-15
\| \| \| \| \| \| \| \|	- Support for empty structs and unions - Better handling of "extern" and "extern inline" function definitions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2493 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Assorted fixes to fix parsing issues and be more GCC-like:	xleroy	2014-05-12
\| \| \| \| \| \| \| \| \| \|	- Moved scanning of char constants and string literals entirely to Lexer - Parser: separate STRING_LITERAL from CONSTANT to be closer to ISO C99 grammar - pre_parser: adapted + "asm" takes string_literal, not CONSTANT - Revised errors "inline doesnt belong here" git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2492 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Incorrect conversion of K&R functions. Example of problem:	xleroy	2014-05-12
\| \| \| \| \| \| \|	void * foo(s, u) ... git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2491 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fix string litteral parsing	jjourdan	2014-05-11
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2490 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Bump	xleroy	2014-05-09
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2489 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fixed regression on initializers of the form T x[N] = "literal";	xleroy	2014-05-08
\| \| \| \| \| \| \|	where T is a typedef for a character type. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2488 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	- Added alternate keywords __inline, __restrict, etc, for GCC compatibility	xleroy	2014-05-08
\| \| \| \| \| \| \|	- Skip comments that might remain after preprocessing git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2487 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update Coq documentation	xleroy	2014-05-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2483 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update for release 2.3.	xleroy	2014-05-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2482 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Fused multiply-add for IA32.	xleroy	2014-05-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2481 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Stern warning on non-prototype function definitions.	xleroy	2014-05-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2480 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Do not allow typedef_name in identifier lists of K&R style definitions	jjourdan	2014-05-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2479 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Support for old-style K&R function definitions.	xleroy	2014-05-05
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2478 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Treat all identifiers as VAR_NAME by default (i.e. if not bound by a ↵	xleroy	2014-05-05
\| \| \| \| \| \|	typedef). This produces better error messages for unbound variable names (proper error message in Elab rather than cryptic syntax error in pre_parser). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2477 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Adapt to the two different calling conventions for floats.	xleroy	2014-05-02
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2476 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	ARM: honor common variables.	xleroy	2014-05-02
\| \| \| \| \| \| \|	Changelog: update. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2475 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	New sub-target: arm-hardfloat	xleroy	2014-05-02
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2474 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Preliminary support for EABI-hardfloat calling conventions	xleroy	2014-05-02
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2473 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Be less picky in the way we parse '#' lines	xleroy	2014-05-02
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2472 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Check availability of tools	xleroy	2014-05-02
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2471 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Bump version number before I forget	xleroy	2014-05-01
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2470 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Integration of Jacques-Henri Jourdan's verified parser.	xleroy	2014-04-29
\| \| \| \| \| \| \|	(Merge of branch newparser.) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Update with post-2.2 changes	xleroy	2014-04-23
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2460 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Clean-up pass on C types:	xleroy	2014-04-23
\| \| \| \| \| \| \| \| \| \| \| \| \|	- Ctypes: add useful functions on attributes; remove attrs in typeconv (because attributes are meaningless on r-values) - C2C: fixed missing or redundant Evalof - Cop: ignore attributes in ptr + int and ptr - int (meaningless on r-values); add sanity check between typeconv/classify_binarith and the C99 standard. - cparser: fixed several cases where incorrect type annotations were put on expressions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2457 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Continued: change typeconv t into incrdecr_type t for Epostincr.	xleroy	2014-04-16
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2456 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Use "incrdecr_type ty" instead of "typeconv ty" as the intermediate type	xleroy	2014-04-15
\| \| \| \| \| \| \|	for Epostincr operations. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2455 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
*	Updated the proofs.	xleroy	2014-04-12
\| \| \| \|	git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2454 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