| Commit message (Expand) | Author | Age | Files | Lines | ||
|---|---|---|---|---|---|---|
| ... | ||||||
| | | * | | | | RISC-V: wrong fixup code generated for vararg calls with fixed FP args | Xavier Leroy | 2021-01-10 | 3 | -12/+35 | |
| | | * | | | | Ignore and warn about pragmas inside functions | Xavier Leroy | 2021-01-07 | 1 | -1/+4 | |
| | | * | | | | Replace `omega` tactic with `lia` | Xavier Leroy | 2020-12-29 | 110 | -2695/+2694 | |
| | | * | | | | Remove useless parameters in theorems int_round_odd_bits and int_round_odd_le | Xavier Leroy | 2020-12-29 | 2 | -13/+13 | |
| | | * | | | | Update Flocq to 3.4.0 (#383) | Guillaume Melquiond | 2020-12-28 | 30 | -638/+1841 | |
| | | * | | | | configure: simplify the final printing of the configuration | Xavier Leroy | 2020-12-28 | 1 | -9/+8 | |
| | | * | | | | configure: add -mandir option (#382) | Daniel Dickman | 2020-12-28 | 1 | -1/+7 | |
| | | * | | | | AArch64 / macOS: use __DATA,__CONST section instead of .const (temporary fix) | Xavier Leroy | 2020-12-26 | 1 | -1/+1 | |
| | | * | | | | AArch64: macOS port | Xavier Leroy | 2020-12-26 | 18 | -220/+570 | |
| | | * | | | | C parser: handle other built-in types than __builtin_va_list | Xavier Leroy | 2020-12-26 | 1 | -1/+2 | |
| | | * | | | | AArch64: clarify the printing of extending-register arithmetic operations | Xavier Leroy | 2020-12-26 | 1 | -13/+13 | |
| | | * | | | | AArch64: wrong function alignment | Xavier Leroy | 2020-12-26 | 1 | -1/+1 | |
| | | * | | | | RISC-V: revised calling conventions for variadic functions | Xavier Leroy | 2020-12-25 | 2 | -63/+105 | |
| | | * | | | | Changed cc_varargs to an option type | Bernhard Schommer | 2020-12-25 | 12 | -27/+36 | |
| | | * | | | | configure: use `$make` instead of `make` | Xavier Leroy | 2020-12-25 | 1 | -1/+1 | |
| | | * | | | | configure script revised and simplified | Xavier Leroy | 2020-12-24 | 1 | -83/+43 | |
| | | * | | | | 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 | 2 | -2/+8 | |
| | | * | | | | x86 32 bits: ABI non-conformance for functions returning structs/unions | Xavier Leroy | 2020-12-11 | 1 | -1/+1 | |
| * | | | | | | omega -> lia | David Monniaux | 2021-06-06 | 2 | -26/+28 | |
| | |_|/ / / |/| | | | | ||||||
| * | | | | | for making the docker | David Monniaux | 2021-05-11 | 4 | -0/+3 | |
| * | | | | | for pruning the docker | David Monniaux | 2021-05-11 | 1 | -1/+2 | |
| * | | | | | pruning the image | David Monniaux | 2021-05-11 | 1 | -0/+4 | |
| * | | | | | adjust to compile for various arch | David Monniaux | 2021-05-11 | 1 | -3/+3 | |
| * | | | | | progress being made | David Monniaux | 2021-05-10 | 1 | -2/+15 | |
| * | | | | | build for aarch64 | David Monniaux | 2021-05-10 | 1 | -1/+4 | |
| * | | | | | dockerfiles | David Monniaux | 2021-05-10 | 2 | -8/+9 | |
| * | | | | | dockerfile for building | David Monniaux | 2021-05-10 | 1 | -0/+8 | |
| * | | | | | Increasing required OCaml version (Pervasives <-> Stdlib module renaming) | Cyril SIX | 2021-05-04 | 1 | -2/+2 | |
| * | | | | | for OCaml 4.13 | David Monniaux | 2021-04-30 | 1 | -1/+1 | |
| * | | | | | Compatibilité Coq 8.13 | David Monniaux | 2021-04-28 | 5 | -8/+3 | |
| * | | | | | add auxfile | David Monniaux | 2021-04-27 | 1 | -0/+17 | |
| * | | | | | Merge branch 'kvx-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCer... | Léo Gourdin | 2021-04-22 | 18 | -566/+370 | |
| |\ \ \ \ \ | ||||||
| | * | | | | | fix broken link in index-kvx.html | Sylvain Boulmé | 2021-04-16 | 1 | -1/+1 | |
| | | |_|_|/ | |/| | | | ||||||
| | * | | | | Merge remote-tracking branch 'origin/manuscript' into kvx-worksubmission_OOPSLA2021_AARCH64_KVX | Cyril SIX | 2021-04-13 | 5 | -525/+173 | |
| | |\ \ \ \ | ||||||
| | | * | | | | Cleaning | Cyril SIX | 2021-04-02 | 1 | -2/+1 | |
| | | * | | | | More efficient | Cyril SIX | 2021-04-02 | 1 | -8/+12 | |
| | | * | | | | Outermost loop detection works | Cyril SIX | 2021-04-02 | 1 | -9/+10 | |
| | | * | | | | Getting all loop bodies | Cyril SIX | 2021-04-02 | 2 | -2/+50 | |
| | | * | | | | get_loop_headers simplification (using the new get_loop_backedges) | Cyril SIX | 2021-04-02 | 1 | -39/+7 | |
| | | * | | | | Simple backedge detection (modified code from get_loop_headers) | Cyril SIX | 2021-04-02 | 3 | -0/+57 | |
| | | * | | | | Big simplification of get_loop_info | Cyril SIX | 2021-03-31 | 1 | -111/+16 | |
| | | * | | | | Simplification of the Linearize heuristic (same result functionally) | Cyril SIX | 2021-03-30 | 1 | -216/+6 | |
| | | * | | | | Simplifications on Linearize - details below | Cyril SIX | 2021-03-29 | 1 | -205/+79 | |
| | | * | | | | Code simplification of get_path_map (no functionality change) | Cyril SIX | 2021-01-26 | 1 | -14/+16 | |
| | * | | | | | Adding more precise heuristic measures | Cyril SIX | 2021-04-13 | 1 | -2/+62 | |
| | * | | | | | Adding overpredicts | Cyril SIX | 2021-04-13 | 1 | -3/+6 | |
| | * | | | | | Recording of prediction stats with COMPCERT_PROFILING_STATS environment flag | Cyril SIX | 2021-04-13 | 1 | -33/+93 | |
| | * | | | | | Adding distinction between kvx-cos and kvx-mbr (for trapping loads) | Cyril SIX | 2021-04-13 | 7 | -4/+22 | |
| | * | | | | | rm spurious files | David Monniaux | 2021-04-12 | 39 | -1705/+0 | |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |