| Commit message (Expand) | Author | Age | Files | Lines |
* | Replace omega by lia | Yann Herklotz | 2023-04-27 | 7 | -52/+57 |
* | Fix dune file as well | Yann Herklotz | 2023-04-27 | 1 | -1/+1 |
* | Add proof of splitlong_ptr32 | Yann Herklotz | 2023-04-27 | 1 | -0/+3 |
* | Add Verilog backend | Yann Herklotz | 2023-04-27 | 33 | -0/+16929 |
* | Always try inlining functions | Yann Herklotz | 2023-04-27 | 1 | -4/+1 |
* | Ignore unnecessary folders | Yann Herklotz | 2023-04-27 | 2 | -1/+1 |
* | Fix a comment in Cstrategy.v (#485) | Xuyang Li | 2023-04-05 | 1 | -2/+2 |
* | Use a shorter insruction on x86 for loading unsigned 32-bit immediates into 6... | Valoran | 2023-04-05 | 1 | -1/+3 |
* | Support Coq 8.16.0 and 8.16.1 in configure script | Xavier Leroy | 2023-03-10 | 1 | -2/+2 |
* | Update warning flags used to compile Flocq and Menhirlib | Xavier Leroy | 2023-03-10 | 1 | -2/+5 |
* | Upgrade Flocq to 4.1.1 | Xavier Leroy | 2023-03-10 | 3 | -15/+15 |
* | Address most deprecation warnings from Coq 8.16 | Xavier Leroy | 2023-03-10 | 5 | -13/+18 |
* | Include `+unix` and `+str` for OCaml 5 compatibility | Xavier Leroy | 2023-03-06 | 1 | -1/+3 |
* | Change preference for new register in allocator | Bernhard Schommer | 2023-03-06 | 7 | -29/+129 |
* | configure: add -ignore-ocaml-version option | Xavier Leroy | 2023-03-05 | 1 | -8/+11 |
* | Fix Thumb handling of `add reg, sp, #imm` and `sub reg, sp, #imm` | Xavier Leroy | 2023-02-20 | 1 | -3/+4 |
* | Move the old `offset_in_range` function inside `memcpy_small_arg` | Bernhard Schommer | 2023-02-20 | 1 | -3/+2 |
* | For Thumb, use `movs` for loading immediate constants | Bernhard Schommer | 2023-02-20 | 1 | -2/+2 |
* | Use more functions from Asmgen in Asmexpand. | Bernhard Schommer | 2023-02-20 | 1 | -17/+4 |
* | Use the Asmgen offset check for volatile load/store. | Bernhard Schommer | 2023-02-20 | 1 | -4/+20 |
* | ARM code generation: fix offset checks for loads | Bernhard Schommer | 2023-02-20 | 1 | -3/+3 |
* | Remove unused definition | Bernhard Schommer | 2023-02-20 | 1 | -4/+0 |
* | When installing the Coq development, also install coq-native generated files | Xavier Leroy | 2023-02-20 | 1 | -1/+6 |
* | Ignore self assign in if-conversion | Bernhard Schommer | 2023-02-20 | 2 | -4/+19 |
* | RISC-V: print flt.s, feq.s, fle.s with a tab after the mnemonic (#481) | David Monniaux | 2023-02-07 | 1 | -3/+3 |
* | wchar_t is unsigned int for arm_littleendian, arm_bigendian and aarch64 | Bernhard Schommer | 2023-02-01 | 1 | -2/+7 |
* | Use define for wchar_t type | Bernhard Schommer | 2023-02-01 | 2 | -6/+11 |
* | Export `name_of_ikind` and `name_of_fkind` | Xavier Leroy | 2023-02-01 | 1 | -0/+3 |
* | Introduce `wchar_ikind` in machine descriptions | Xavier Leroy | 2023-01-24 | 4 | -20/+12 |
* | Don't discard argument of `__builtin_va_end` | Michael Schmidt | 2023-01-23 | 1 | -2/+2 |
* | Disable tail calls in variadic functions | Michael Schmidt | 2023-01-23 | 2 | -5/+6 |
* | Elaboration of compound initializers: reverse list of generated global variables | Michael Schmidt | 2023-01-23 | 1 | -1/+1 |
* | C2C: wrong handling of typedefs to enums in bit fields | Xavier Leroy | 2023-01-23 | 1 | -1/+1 |
* | Use `exfalso` instead of `elimtype False` (#470) | Pierre-Marie Pédrot | 2022-12-22 | 5 | -7/+7 |
* | Remove support for 32-bit Cygwin | Xavier Leroy | 2022-12-08 | 2 | -23/+7 |
* | Update doc comment | Xavier Leroy | 2022-12-08 | 1 | -2/+2 |
* | Fix incomplete checking of unsolved holes (#465) | Gaëtan Gilbert | 2022-11-28 | 1 | -1/+1 |
* | Updates for release 3.12 | Xavier Leroy | 2022-11-21 | 3 | -3/+54 |
* | Emit the Tag_ABI_VFP attribute appropriate to the calling conventions used | Xavier Leroy | 2022-11-21 | 1 | -1/+6 |
* | configure: add option -sharedir to specify where to put compcert.ini (#460) | Xavier Leroy | 2022-11-14 | 1 | -5/+32 |
* | Wrong test for coroutined decompressor | Xavier Leroy | 2022-11-14 | 1 | -1/+1 |
* | Merge pull request #459 from AbsInt/full-switch | Xavier Leroy | 2022-11-09 | 13 | -142/+500 |
|\ |
|
| * | Ignore debug statements before the first case of a `switch` | Xavier Leroy | 2022-11-03 | 1 | -1/+7 |
| * | Update man-page for `-funstructured-switch` (also for new `-std` option, `-fi... | Michael Schmidt | 2022-11-03 | 1 | -4/+22 |
| * | Handle unstructured 'switch' statements such as Duff's device | Xavier Leroy | 2022-10-29 | 12 | -98/+439 |
| * | Unblock: never put debug info before a label | Xavier Leroy | 2022-10-29 | 1 | -11/+12 |
| * | Revised passing of options to `Parse.preprocessed_file` | Xavier Leroy | 2022-09-27 | 3 | -41/+33 |
* | | Replace CR, FF and VT with whitespace. | Bernhard Schommer | 2022-11-05 | 1 | -3/+5 |
* | | Use open_in_bin instead of open_in. | Bernhard Schommer | 2022-11-05 | 1 | -1/+1 |
* | | Merge pull request #458 from AbsInt/simpl-expr-dests | Xavier Leroy | 2022-10-24 | 6 | -99/+220 |
|\ \ |
|