Commit message (Expand) | Author | Age | Files | Lines | ||
---|---|---|---|---|---|---|
... | ||||||
| | * | timing | David Monniaux | 2021-06-07 | 2 | -0/+117 | |
| | * | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | David Monniaux | 2021-06-06 | 340 | -6016/+11801 | |
| | |\ | ||||||
| | | * | Remove install path bricolage for kvxv3.9_kvx | Cyril SIX | 2021-06-01 | 2 | -4/+5 | |
| | | * | Merge remote-tracking branch 'verimag/manuscript' into kvx-work | Cyril SIX | 2021-06-01 | 1 | -13/+11 | |
| | | |\ | ||||||
| | | | * | Do not rotate if the CB was already at the end. | Cyril SIX | 2021-04-28 | 1 | -1/+5 | |
| | | | * | Heuristic counter update | Cyril SIX | 2021-04-28 | 1 | -12/+6 | |
| | | * | | Update INSTALL.md | Cyril SIX | 2021-06-01 | 1 | -0/+6 | |
| | | * | | Fixing build for KVX (missing ccomp_kvx_fixes.h for runtime) | Cyril SIX | 2021-06-01 | 1 | -0/+1 | |
| | | * | | Add target ELF | Cyril SIX | 2021-06-01 | 4 | -2/+7 | |
| | | * | | Merge remote-tracking branch 'absint/master' into kvx-work | Cyril SIX | 2021-06-01 | 3 | -4/+6 | |
| | | |\ \ | ||||||
| | | | * | | Support `# 0 ...` preprocessed line directive | Xavier Leroy | 2021-06-01 | 1 | -1/+1 | |
| | | | * | | Register X1 is destroyed by some built-in functions | Xavier Leroy | 2021-05-13 | 2 | -3/+5 | |
| | | | * | | Update for release 3.9 | Xavier Leroy | 2021-05-10 | 1 | -1/+1 | |
| | | | * | | Update Changelog for release 3.9 | Xavier Leroy | 2021-05-09 | 1 | -0/+3 | |
| | | | * | | Update for release 3.9 | Xavier Leroy | 2021-05-09 | 1 | -4/+5 | |
| | | | * | | Update Changelog | Xavier Leroy | 2021-05-08 | 1 | -1/+11 | |
| | | | * | | Use the LGPL instead of the GPL for dual-licensed files | Xavier Leroy | 2021-05-08 | 149 | -860/+1171 | |
| | | | * | | Fix evaluation order in emulation of bitfield assignment | Xavier Leroy | 2021-05-02 | 1 | -2/+2 | |
| | | | * | | Support __builtin_expect | Xavier Leroy | 2021-05-02 | 1 | -0/+5 | |
| | | | * | | Support __builtin_unreachable | Xavier Leroy | 2021-05-02 | 8 | -2/+32 | |
| | | | * | | Fix spurious error on initialization of struct with flexible array member | Xavier Leroy | 2021-05-02 | 1 | -0/+3 | |
| | | | * | | Update Changelog | Xavier Leroy | 2021-04-29 | 1 | -0/+53 | |
| | | | * | | Emit no entry for variables without init in json. | Bernhard Schommer | 2021-04-29 | 1 | -1/+7 | |
| | | | * | | MacOS: add a #define __DARWIN_OS_INLINE | Xavier Leroy | 2021-04-27 | 1 | -2/+2 | |
| | | | * | | Support Coq 8.13.2 | Xavier Leroy | 2021-04-27 | 1 | -2/+2 | |
| | | | * | | More fixes for ld/std issue. | Bernhard Schommer | 2021-04-24 | 1 | -11/+40 | |
| | | | * | | Tentative first fix for offsets of ld/std. | Bernhard Schommer | 2021-04-24 | 5 | -152/+259 | |
| | | | * | | Update the output of clightgen to pick the `$` notation from its new place | Xavier Leroy | 2021-04-23 | 1 | -1/+3 | |
| | | | * | | Remove `-version-file` option from option summary | Xavier Leroy | 2021-04-23 | 1 | -1/+0 | |
| | | | * | | Move `$` notation in submodule `ClightNotations` and scope `clight_scope` | Xavier Leroy | 2021-04-23 | 1 | -11/+23 | |
| | | | * | | Use List.repeat from Coq's standard library instead of list_repeat | Xavier Leroy | 2021-04-19 | 4 | -36/+16 | |
| | | | * | | Bump minimal Coq version to 8.9.0 | Xavier Leroy | 2021-04-19 | 1 | -2/+2 | |
| | | | * | | Elab bitfields: check size of type <=32bit rather than checking rank (#387) | Amos Robinson | 2021-04-19 | 4 | -2/+25 | |
| | | | * | | Refactor cparser/Parse.ml | Xavier Leroy | 2021-04-19 | 1 | -31/+29 | |
| | | | * | | Ensure compatibility with future versions of MenhirLib | Xavier Leroy | 2021-04-19 | 1 | -6/+7 | |
| | | | * | | Do not depend on projection parameter names (#388) | Xia Li-yao | 2021-03-25 | 1 | -1/+1 | |
| | | * | | | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1 | Cyril SIX | 2021-06-01 | 77 | -1940/+4260 | |
| | | |\ \ \ | ||||||
| | | | * | | | removing some Expansion when loading float/single constants | Léo Gourdin | 2021-06-01 | 1 | -16/+22 | |
| | | | * | | | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | Léo Gourdin | 2021-05-31 | 1 | -1/+0 | |
| | | | |\ \ \ | ||||||
| | | | | * | | | just remove a debug print | Léo Gourdin | 2021-05-29 | 1 | -1/+0 | |
| | | | * | | | | bugfix A64 peephole (cf Scade/Fighter example) | Léo Gourdin | 2021-05-31 | 1 | -6/+5 | |
| | | | |/ / / | ||||||
| | | * | | | | Commenting out __builtin_expect from AbsInt | Cyril SIX | 2021-06-01 | 1 | -2/+2 | |
| | | * | | | | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in cfrontend... | Cyril SIX | 2021-06-01 | 167 | -1119/+1692 | |
| | | * | | | | Updating varargs2 results for kvx | Cyril SIX | 2021-06-01 | 1 | -0/+1 | |
| | | * | | | | Remove /home/yuki/Work/VERIMAG/CompCert | Cyril SIX | 2021-06-01 | 1 | -1/+1 | |
| | | * | | | | fix aarch64 merge? | Léo Gourdin | 2021-03-29 | 7 | -846/+19 | |
| | | * | | | | replacing omega with lia in some file | Léo Gourdin | 2021-03-29 | 33 | -267/+296 | |
| | | * | | | | fix riscv merge? | Léo Gourdin | 2021-03-29 | 5 | -488/+0 | |
| | | * | | | | fix CI arm and armhf | Sylvain Boulmé | 2021-03-24 | 1 | -2/+6 | |
| | | * | | | | Merge branch 'master' into merge_master_8.13.1 | Sylvain Boulmé | 2021-03-23 | 201 | -4415/+9534 | |
| | | |\ \ \ \ | | | | | |/ / | | | | |/| | |