summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Use VFD regs to implement 64-bit mem-mem copies in builtin_memcpy_false.Gravatar xleroy2014-08-21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2616 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support C99 compound literals (by expansion in Unblock pass).Gravatar xleroy2014-08-21
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2615 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Follow-up to commit 2613Gravatar xleroy2014-08-20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2614 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add builtins for load with reservation and conditional store.Gravatar xleroy2014-08-20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2613 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong types for strex builtins.Gravatar xleroy2014-08-20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2612 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Better validation of target for ARMGravatar xleroy2014-08-20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2611 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Obvious typos in commit r2609Gravatar xleroy2014-08-20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2610 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add some more synchronization builtinsGravatar xleroy2014-08-20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2609 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improve error reporting for unsupported compound literals.Gravatar xleroy2014-08-20
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2608 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Excessively strict validation: ofs + sz < modulus should have beenGravatar xleroy2014-08-20
| | | | | | | ofs + sz <= modulus. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2607 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Rename "-fthumb" option into "-mthumb" for GCC compatibility.Gravatar xleroy2014-08-19
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2572 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* checklink/Check.ml: missing SDA addressing for store instructions.Gravatar xleroy2014-08-19
| | | | | | | | powerpc/PrintAsm.ml: update Linux output (Csymbol_rel, SDA sections). test/regression/sections.c: test for SDA and relative addressings. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2571 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update dependenciesGravatar xleroy2014-08-19
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2570 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc/Asm: simplify the modeling of Csymbol_low and Csymbol_high.Gravatar xleroy2014-08-18
| | | | | | | | | | | powerpc/Asmgen*: simplify the code generated for far-data relative accesses, so that the only occurrences of Csymbol_rel_{low,high} are in the pattern Paddis(r, GPR0, Csymbol_rel_high...); Paddi(r, r, Csymbol_rel_low...) checklink/Check.ml: check the pattern above. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2569 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Improve error detection and error messages for enums.Gravatar xleroy2014-08-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2568 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Issue with switch labels that are negative 32-bit integers.Gravatar xleroy2014-08-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2567 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add some tests for "switch" over 32 and 64-bit integers.Gravatar xleroy2014-08-17
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2566 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* - Support "switch" statements over 64-bit integersGravatar xleroy2014-08-17
| | | | | | | | | | | | | (in CompCert C to Cminor, included) - Translation of "switch" to decision trees or jumptables made generic over the sizes of integers and moved to the Cminor->CminorSel pass instead of CminorSel->RTL as before. - CminorSel: add "exitexpr" to support the above. - ValueDomain: more precise analysis of comparisons against an integer literal. E.g. "x >=u 0" is always true. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2565 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Nicer reporting of I/O errors (e.g. "No such file").Gravatar xleroy2014-08-13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2564 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Spurious error on a local static function declarationGravatar xleroy2014-08-13
| | | | | | | ("static int f(void);" inside a function). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2563 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update commentGravatar xleroy2014-08-13
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2562 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Add Mem.free_parallel_inject and use it to simplify Events a bit.Gravatar xleroy2014-07-31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2556 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* configure: distinguish between ABI and processor model.Gravatar xleroy2014-07-29
| | | | | | | | ARM: various tweaks, incl. support for SDIV and UDIV insns when available. test/regression/funptr2.c: Thumb does weird things with <function ptr>+1. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* All targets: add __builtin_membarGravatar xleroy2014-07-28
| | | | | | | ARM: add __builtin_dsb __builtin_isb git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2554 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* PowerPC port: refactored the expansion of built-in functions andGravatar xleroy2014-07-28
| | | | | | | | | | pseudo-instructions so that it does not need to be re-done in cchecklink. cchecklink: updated accordingly. testsuite: compile with -sdump and run cchecklink if supported. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2553 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Updated ChangelogGravatar xleroy2014-07-28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2552 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* The NaN behavior of float_of_single differs on PowerPC and on IA32/ARM.Gravatar xleroy2014-07-28
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2550 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM port: add support for Thumb2. To be tested.Gravatar xleroy2014-07-27
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2549 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update for single-precision floats. Calls to vararg functions remainGravatar xleroy2014-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.Gravatar xleroy2014-07-23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2543 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update with _a memory accessesGravatar xleroy2014-07-23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2542 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplify COQINCLUDESGravatar xleroy2014-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.Gravatar xleroy2014-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 CAMLINCLUDESGravatar xleroy2014-07-23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2539 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Update "read_as_zeros" property.Gravatar xleroy2014-07-23
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2538 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of "newspilling" branch:Gravatar xleroy2014-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.Gravatar xleroy2014-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 installedGravatar jjourdan2014-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 worksGravatar jjourdan2014-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.Gravatar xleroy2014-06-30
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2519 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Document commit r2507.Gravatar xleroy2014-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.Gravatar xleroy2014-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 ↵Gravatar xleroy2014-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.Gravatar xleroy2014-05-24
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2503 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Empty declarationsGravatar jjourdan2014-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.Gravatar xleroy2014-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" }Gravatar xleroy2014-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.Gravatar xleroy2014-05-18
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2497 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* BumpGravatar xleroy2014-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.Gravatar xleroy2014-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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 01:29:24 +0000