Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | 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 |
* | | | | | csmith | creduce breaks on RISC-V 64 | David Monniaux | 2021-09-22 | 1 | -0/+36 |
* | | | | | fix typo | David Monniaux | 2021-09-21 | 1 | -1/+1 |
* | | | | | grep for ASAN errors | David Monniaux | 2021-09-21 | 1 | -5/+9 |
* | | | | | do not allow arbitrary conversions | David Monniaux | 2021-09-21 | 1 | -4/+4 |
|/ / / / | |||||
* | | | | no packed struct | David Monniaux | 2021-09-21 | 1 | -1/+1 |