aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Update verilog back end with new x86 changesHEADmasterYann Herklotz2023-04-2721-165/+475
* Fix compilation of verilog back endYann Herklotz2023-04-272-102/+77
* Replace omega by liaYann Herklotz2023-04-277-52/+57
* Fix dune file as wellYann Herklotz2023-04-271-1/+1
* Add proof of splitlong_ptr32Yann Herklotz2023-04-271-0/+3
* Add Verilog backendYann Herklotz2023-04-2733-0/+16929
* Always try inlining functionsYann Herklotz2023-04-271-4/+1
* Ignore unnecessary foldersYann Herklotz2023-04-272-1/+1
* Fix a comment in Cstrategy.v (#485)Xuyang Li2023-04-051-2/+2
* Use a shorter insruction on x86 for loading unsigned 32-bit immediates into 6...Valoran2023-04-051-1/+3
* Support Coq 8.16.0 and 8.16.1 in configure scriptXavier Leroy2023-03-101-2/+2
* Update warning flags used to compile Flocq and MenhirlibXavier Leroy2023-03-101-2/+5
* Upgrade Flocq to 4.1.1Xavier Leroy2023-03-103-15/+15
* Address most deprecation warnings from Coq 8.16Xavier Leroy2023-03-105-13/+18
* Include `+unix` and `+str` for OCaml 5 compatibilityXavier Leroy2023-03-061-1/+3
* Change preference for new register in allocatorBernhard Schommer2023-03-067-29/+129
* configure: add -ignore-ocaml-version optionXavier Leroy2023-03-051-8/+11
* Fix Thumb handling of `add reg, sp, #imm` and `sub reg, sp, #imm`Xavier Leroy2023-02-201-3/+4
* Move the old `offset_in_range` function inside `memcpy_small_arg`Bernhard Schommer2023-02-201-3/+2
* For Thumb, use `movs` for loading immediate constantsBernhard Schommer2023-02-201-2/+2
* Use more functions from Asmgen in Asmexpand.Bernhard Schommer2023-02-201-17/+4
* Use the Asmgen offset check for volatile load/store.Bernhard Schommer2023-02-201-4/+20
* ARM code generation: fix offset checks for loadsBernhard Schommer2023-02-201-3/+3
* Remove unused definitionBernhard Schommer2023-02-201-4/+0
* When installing the Coq development, also install coq-native generated filesXavier Leroy2023-02-201-1/+6
* Ignore self assign in if-conversionBernhard Schommer2023-02-202-4/+19
* RISC-V: print flt.s, feq.s, fle.s with a tab after the mnemonic (#481)David Monniaux2023-02-071-3/+3
* wchar_t is unsigned int for arm_littleendian, arm_bigendian and aarch64Bernhard Schommer2023-02-011-2/+7
* Use define for wchar_t typeBernhard Schommer2023-02-012-6/+11
* Export `name_of_ikind` and `name_of_fkind`Xavier Leroy2023-02-011-0/+3
* Introduce `wchar_ikind` in machine descriptionsXavier Leroy2023-01-244-20/+12
* Don't discard argument of `__builtin_va_end`Michael Schmidt2023-01-231-2/+2
* Disable tail calls in variadic functionsMichael Schmidt2023-01-232-5/+6
* Elaboration of compound initializers: reverse list of generated global variablesMichael Schmidt2023-01-231-1/+1
* C2C: wrong handling of typedefs to enums in bit fieldsXavier Leroy2023-01-231-1/+1
* Use `exfalso` instead of `elimtype False` (#470)Pierre-Marie Pédrot2022-12-225-7/+7
* Remove support for 32-bit CygwinXavier Leroy2022-12-082-23/+7
* Update doc commentXavier Leroy2022-12-081-2/+2
* Fix incomplete checking of unsolved holes (#465)Gaëtan Gilbert2022-11-281-1/+1
* Updates for release 3.12Xavier Leroy2022-11-213-3/+54
* Emit the Tag_ABI_VFP attribute appropriate to the calling conventions usedXavier Leroy2022-11-211-1/+6
* configure: add option -sharedir to specify where to put compcert.ini (#460)Xavier Leroy2022-11-141-5/+32
* Wrong test for coroutined decompressorXavier Leroy2022-11-141-1/+1
* Merge pull request #459 from AbsInt/full-switchXavier Leroy2022-11-0913-142/+500
|\
| * Ignore debug statements before the first case of a `switch`Xavier Leroy2022-11-031-1/+7
| * Update man-page for `-funstructured-switch` (also for new `-std` option, `-fi...Michael Schmidt2022-11-031-4/+22
| * Handle unstructured 'switch' statements such as Duff's deviceXavier Leroy2022-10-2912-98/+439
| * Unblock: never put debug info before a labelXavier Leroy2022-10-291-11/+12
| * Revised passing of options to `Parse.preprocessed_file`Xavier Leroy2022-09-273-41/+33
* | Replace CR, FF and VT with whitespace.Bernhard Schommer2022-11-051-3/+5