| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10 | David Monniaux | 2021-09-27 | 27 | -694/+1098 |
| |\ | |||||
| | * | Merge pull request #413 from AbsInt/new-export | Xavier Leroy | 2021-09-27 | 27 | -694/+1098 |
| | |\ | |||||
| | | * | Update export/README.md | Xavier Leroy | 2021-09-22 | 1 | -18/+18 |
| | | * | Add support to clightgen for generating Csyntax AST as .v files | Xavier Leroy | 2021-09-22 | 21 | -271/+625 |
| | | * | Refactor clightgen | Xavier Leroy | 2021-09-22 | 13 | -594/+644 |
| * | | | Merge branch 'bitfields_fix' of /home/monniaux/work/Kalray/bitfields_fix into... | David Monniaux | 2021-09-27 | 2 | -3/+80 |
| |\ \ \ | |||||
| | * | | | generate insf | David Monniaux | 2021-09-27 | 1 | -32/+32 |
| | * | | | tests in another way | David Monniaux | 2021-09-27 | 1 | -10/+10 |
| | * | | | more cases detected | David Monniaux | 2021-09-27 | 1 | -1/+33 |
| | * | | | progress in selectop | David Monniaux | 2021-09-27 | 1 | -4/+4 |
| | * | | | progress in selectop | David Monniaux | 2021-09-27 | 1 | -1/+9 |
| | * | | | recognize insf (missing one case) | David Monniaux | 2021-09-27 | 2 | -0/+37 |
| * | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10 | David Monniaux | 2021-09-26 | 6 | -39/+25 |
| |\ \ \ \ | | |/ / | |/| | | |||||
| | * | | | Vendored MenhirLib: replace Require Omega with Require ZArith | Xavier Leroy | 2021-09-25 | 1 | -1/+1 |
| | * | | | Update the vendored Flocq library to version 3.4.2 | Xavier Leroy | 2021-09-25 | 5 | -38/+24 |
| * | | | | same changes as for RISC-V | David Monniaux | 2021-09-24 | 1 | -2/+2 |
| * | | | | Merge remote-tracking branch 'origin/csmith' into towards_3.10 | David Monniaux | 2021-09-24 | 3 | -3/+25 |
| |\ \ \ \ | |||||
| | * | | | | rm spurious comment | David Monniaux | 2021-09-23 | 1 | -1/+0 |
| | * | | | | Merge branch 'csmith' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ... | David Monniaux | 2021-09-23 | 16 | -33/+271 |
| | |\ \ \ \ | |||||
| | | * | | | | reactivate csmith on rv64 after bugfix | David Monniaux | 2021-09-23 | 1 | -1/+1 |
| | | * | | | | Merge remote-tracking branch 'origin/kvx-work' into csmith | David Monniaux | 2021-09-23 | 1 | -2/+2 |
| | | |\ \ \ \ | | | | |/ / | | | |/| | | |||||
| | | * | | | | it did not compile on AArch64 | David Monniaux | 2021-09-23 | 1 | -2/+2 |
| | | * | | | | Fix wrong expansion of __builtin_memcpy_aligned | Xavier Leroy | 2021-09-23 | 4 | -8/+8 |
| | * | | | | | union passing | David Monniaux | 2021-09-23 | 1 | -0/+23 |
| | * | | | | | add union passing | David Monniaux | 2021-09-23 | 1 | -1/+1 |
| * | | | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10 | David Monniaux | 2021-09-24 | 64 | -2568/+4388 |
| |\ \ \ \ \ \ | |_|_|/ / / |/| | | / / | | |_|/ / | |/| | | | |||||
| | * | | | | Fix wrong expansion of __builtin_memcpy_aligned | Xavier Leroy | 2021-09-23 | 4 | -8/+8 |
| | * | | | | For __builtin_memcpy_aligned, watch out for alignment of stack offsets | Xavier Leroy | 2021-09-23 | 1 | -0/+1 |
| | | |_|/ | |/| | | |||||
| | * | | | Fix the type and the semantics of BI_bsel | Xavier Leroy | 2021-09-22 | 1 | -4/+17 |
| | * | | | For numerical builtins, support return types that are small integer types | Xavier Leroy | 2021-09-22 | 1 | -25/+47 |
| | * | | | Avoid `Global Set Asymmetric Patterns` (#408) | Xavier Leroy | 2021-09-15 | 8 | -5/+13 |
| | * | | | clightgen: handle empty names given to padding bit fields | Xavier Leroy | 2021-09-15 | 2 | -16/+28 |
| | * | | | Handle the new warnings of OCaml 4.13 | Xavier Leroy | 2021-09-13 | 2 | -4/+4 |
| | * | | | Share code for memory access for PowerPC | Bernhard Schommer | 2021-09-06 | 4 | -166/+159 |
| | * | | | Protect against overflows in `leaq` (all forms) | Bernhard Schommer | 2021-08-27 | 1 | -22/+27 |
| | * | | | Protect against overflows in `leaq N(src), dst` (#407) | Xavier Leroy | 2021-08-27 | 1 | -12/+17 |
| | * | | | Merge branch 'bitfields' (#400) | Xavier Leroy | 2021-08-22 | 45 | -2305/+4004 |
| | |\ \ \ | |||||
| | | * | | | Native support for bit fields (#400) | Xavier Leroy | 2021-08-22 | 42 | -2299/+3866 |
| | | * | | | Add Ctypes.link_match_program_gen | Xavier Leroy | 2021-08-22 | 1 | -0/+52 |
| | | * | | | Int.sign_ext_shr_shl: weaker hypothesis | Xavier Leroy | 2021-08-22 | 3 | -6/+6 |
| | | * | | | Add `floor` and some properties | Xavier Leroy | 2021-07-26 | 1 | -0/+37 |
| | | * | | | More lemmas about `align` | Xavier Leroy | 2021-07-26 | 1 | -0/+17 |
| | | * | | | More lemmas about list append | Xavier Leroy | 2021-07-26 | 1 | -0/+26 |
| | * | | | | Revise the declaration of __compcert_* helper functions | Xavier Leroy | 2021-06-30 | 1 | -82/+79 |
| * | | | | | fix for running x86-64 | David Monniaux | 2021-09-23 | 1 | -2/+2 |
| | |_|_|/ |/| | | | |||||
| * | | | | increase timeout for running under simulator, swap yarpgen and csmith | David Monniaux | 2021-09-23 | 1 | -1/+1 |
| * | | | | try with even more stack | David Monniaux | 2021-09-23 | 2 | -2/+2 |
| * | | | | csmith disabled on riscv64 | David Monniaux | 2021-09-22 | 1 | -1/+2 |
| * | | | | Merge branch 'csmith' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ... | David Monniaux | 2021-09-22 | 1 | -4/+5 |
| |\ \ \ \ | |||||
| | * | | | | attempt at printing stuff | David Monniaux | 2021-09-21 | 1 | -4/+5 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |