| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx_fp_division | David Monniaux | 2022-02-12 | 1 | -0/+1 |
| |\ | |||||
| | * | unsigned long -> float without function calls | David Monniaux | 2022-02-12 | 1 | -0/+1 |
| | | | |||||
| * | | Merge ../kvx-work into kvx_fp_division | David Monniaux | 2022-02-03 | 1 | -2/+2 |
| |\| | |||||
| | * | Merge remote-tracking branch 'absint/master' into merge_absint | David Monniaux | 2022-02-02 | 1 | -2/+2 |
| | |\ | |||||
| | | * | Support Coq 8.15.0 | Xavier Leroy | 2022-01-31 | 1 | -2/+2 |
| | | | | |||||
| * | | | add FPDivision64 | David Monniaux | 2022-01-10 | 1 | -1/+1 |
| | | | | |||||
| * | | | Merge remote-tracking branch 'origin/kvx-work' into kvx_fp_division | David Monniaux | 2022-01-07 | 1 | -0/+1 |
| |\| | | |||||
| | * | | ccomp profiling | Léo Gourdin | 2022-01-05 | 1 | -0/+1 |
| | | | | |||||
| * | | | fix configure for kvx | David Monniaux | 2021-12-21 | 1 | -1/+2 |
| |/ / | |||||
| * | | Merge remote-tracking branch 'absint/master' into towards_3.10 | David Monniaux | 2021-12-01 | 1 | -1/+1 |
| |\| | | | | | | | Mostly changes in PTree | ||||
| | * | Support Coq 8.14.1 | Xavier Leroy | 2021-11-26 | 1 | -2/+2 |
| | | | |||||
| * | | Coq 8.14.1 is allowed. | David Monniaux | 2021-12-01 | 1 | -1/+1 |
| | | | |||||
| * | | Merge remote-tracking branch 'origin/master' into towards_3.10 | David Monniaux | 2021-10-29 | 1 | -7/+7 |
| |\| | |||||
| | * | Explicitly remove __SIZEOF_INT128__ macro definition. (#419) | roconnor-blockstream | 2021-10-16 | 1 | -4/+4 |
| | | | | | | | | | | | | | | | | | CompCert does not support 128-bit integers, but the gcc and clang preprocessors do include support as part of its 'built-in'. A common way of testing for 128-bit integer support is to check to see if `__SIZEOF_INT128__` is defined. Eliminating this macro prevents software from believing that 128-bit integers are supported. | ||||
| | * | Add Coq 8.14.0 to the supported versions of Coq | Xavier Leroy | 2021-10-03 | 1 | -3/+3 |
| | | | |||||
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10 | David Monniaux | 2021-09-27 | 1 | -2/+2 |
| |\| | |||||
| | * | Refactor clightgen | Xavier Leroy | 2021-09-22 | 1 | -2/+2 |
| | | | | | | | | | | | | | | | Split reusable parts of ExportClight.ml off, into ExportBase.ml and ExportCtypes.ml. Rename exportclight/ directory to export/ | ||||
| | * | Use the LGPL instead of the GPL for dual-licensed files | Xavier Leroy | 2021-05-08 | 1 | -4/+5 |
| | | | | | | | | | | | | | The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate. | ||||
| | * | MacOS: add a #define __DARWIN_OS_INLINE | Xavier Leroy | 2021-04-27 | 1 | -2/+2 |
| | | | | | | | | | | | Seems necessary for the standard headers of a recent version of XCode. The actual definition in the standard headers is only for GNUC. | ||||
| | * | Support Coq 8.13.2 | Xavier Leroy | 2021-04-27 | 1 | -2/+2 |
| | | | |||||
| | * | Bump minimal Coq version to 8.9.0 | Xavier Leroy | 2021-04-19 | 1 | -2/+2 |
| | | | | | | | | | This is required to have List.repeat in the standard library (next commit). | ||||
| * | | Merge branch 'kvx-work' into BTL | Léo Gourdin | 2021-06-10 | 1 | -110/+94 |
| |\ \ | |||||
| | * | | Remove install path bricolage for kvxv3.9_kvx | Cyril SIX | 2021-06-01 | 1 | -2/+0 |
| | | | | |||||
| | * | | Add target ELF | Cyril SIX | 2021-06-01 | 1 | -2/+3 |
| | | | | |||||
| | * | | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1 | Cyril SIX | 2021-06-01 | 1 | -2/+3 |
| | |\ \ | |||||
| | * | | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵ | Cyril SIX | 2021-06-01 | 1 | -8/+9 |
| | | | | | | | | | | | | | | | | | cfrontend/C2C.ml | ||||
| | * | | | Merge branch 'master' into merge_master_8.13.1 | Sylvain Boulmé | 2021-03-23 | 1 | -102/+86 |
| | |\ \ \ | | | |/ | | |/| | | | | | | | | | | | | | | | | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed | ||||
| | | * | | Coq 8.13.1 is supported | Xavier Leroy | 2021-03-09 | 1 | -2/+2 |
| | | | | | | | | | | | | | | | | | Closes: #389 | ||||
| | | * | | "macosx" is now called "macos" | Xavier Leroy | 2021-01-18 | 1 | -8/+8 |
| | | | | | | | | | | | | | | | | | | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos". | ||||
| | | * | | macOS: turn #warning off | Xavier Leroy | 2021-01-18 | 1 | -2/+2 |
| | | | | | | | | | | | | | | | | | | | | | The standard includes print irrelevant warnings using `#warning`. The warnings can be restored by passing `-W#warning` to `ccomp`. | ||||
| | | * | | Coq 8.13.0 is supported | Xavier Leroy | 2021-01-14 | 1 | -3/+3 |
| | | | | | | | | | | | | | | | | | However it produces new warnings that should be investigated later. | ||||
| | | * | | configure: simplify the final printing of the configuration | Xavier Leroy | 2020-12-28 | 1 | -9/+8 |
| | | | | | | | | | | | | | | | | | | | | | Factor out the substitution of `$prefix` for `\$(PREFIX)` using a shell function `expandprefix`. | ||||
| | | * | | configure: add -mandir option (#382) | Daniel Dickman | 2020-12-28 | 1 | -1/+7 |
| | | | | | | | | | | | | | | | | | | | | | To control where man pages are installed. The default `/usr/local/share/man` is good for Linux but BSD prefers `/usr/local/man`. | ||||
| | | * | | AArch64: macOS port | Xavier Leroy | 2020-12-26 | 1 | -0/+13 |
| | | | | | | | | | | | | | | | | | | | | | This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors. | ||||
| | | * | | configure: use `$make` instead of `make` | Xavier Leroy | 2020-12-25 | 1 | -1/+1 |
| | | | | | | | | | | | | | | | | | | | | | | | | | To make sure it works if `gmake` is required. Fixes: #381 | ||||
| | | * | | configure script revised and simplified | Xavier Leroy | 2020-12-24 | 1 | -83/+43 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Start from reasonable defaults before updating them per-target. Print more details in the final configuration summary. Update the "manual" mode. | ||||
| | | * | | configure: support Coq 8.12.2 | Xavier Leroy | 2020-12-24 | 1 | -2/+2 |
| | | | | | |||||
| | | * | | Configure the correct archiver to build runtime/libcompcert.a | Xavier Leroy | 2020-12-24 | 1 | -1/+7 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Use `${toolprefix}ar` instead of `ar` so as to match the choice of C compiler (as proposed by Michael Soegtrop in PR #380) - Use the Diab archiver `dar` if configured for powerpc-eabi-diab Closes: #380 | ||||
| * | | | | Merge branch 'kvx-work' into BTL | Léo Gourdin | 2021-05-19 | 1 | -2/+2 |
| |\ \ \ \ | | |_|/ | |/| | | |||||
| | * | | | Increasing required OCaml version (Pervasives <-> Stdlib module renaming) | Cyril SIX | 2021-05-04 | 1 | -2/+2 |
| | | | | | |||||
| * | | | | start the new "BTL" IR. | Sylvain Boulmé | 2021-04-28 | 1 | -1/+1 |
| |/ / / | |||||
| * / / | Adding distinction between kvx-cos and kvx-mbr (for trapping loads) | Cyril SIX | 2021-04-13 | 1 | -0/+1 |
| |/ / | |||||
| * | | begin implementing select | David Monniaux | 2021-02-02 | 1 | -0/+1 |
| | | | |||||
| * | | fix Makefile / configure | David Monniaux | 2021-02-01 | 1 | -0/+6 |
| | | | |||||
| * | | directory postpass_lib | Sylvain Boulmé | 2021-01-07 | 1 | -3/+3 |
| | | | |||||
| * | | recreate abstractbb/ | Sylvain Boulmé | 2021-01-07 | 1 | -2/+2 |
| | | | |||||
| * | | cleaning | Sylvain Boulmé | 2021-01-07 | 1 | -1/+1 |
| | | | |||||
| * | | Merge remote-tracking branch 'origin/aarch64-asmblockgenproof' into ↵ | Léo Gourdin | 2020-12-20 | 1 | -2/+2 |
| |\ \ | | | | | | | | | | aarch64-peephole | ||||
| | * | | intermediatet commit before builtins | Léo Gourdin | 2020-12-16 | 1 | -1/+1 |
| | | | | |||||
| | * | | Removing the PseudoAsm IR | Léo Gourdin | 2020-12-13 | 1 | -2/+2 |
| | | | | |||||
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |