1. 30 Jul, 2020 1 commit
  2. 29 Jul, 2020 1 commit
    • Xavier Leroy's avatar
      Remove support for x86-32 under macOS · 338509ae
      Xavier Leroy authored
      32-bit executables cannot be built since XCode 10.0 (sep 2018).
      32-bit executables cannot be executed since MacOS 10.15 (oct 2019).
      Better remove x86-32 support and fail at configuration time instead of
      at the end of the build.
  3. 27 Jul, 2020 9 commits
  4. 21 Jul, 2020 6 commits
  5. 20 Jul, 2020 1 commit
  6. 15 Jul, 2020 3 commits
  7. 09 Jul, 2020 1 commit
  8. 08 Jul, 2020 6 commits
  9. 07 Jul, 2020 2 commits
  10. 01 Jul, 2020 2 commits
  11. 30 Jun, 2020 1 commit
  12. 28 Jun, 2020 4 commits
    • Bernhard Schommer's avatar
      Move shared code in new file. · ad2ea9c2
      Bernhard Schommer authored
      The name_of_register and register_of_name function are shared between
      all architectures and can be moved in a common file.
    • Bernhard Schommer's avatar
      Remove the `can_reserve_register` function. · faa1d7fb
      Bernhard Schommer authored
      The function is in fact just a call to the
      function`is_callee_save_register` from `Conventions1.v`.
    • Bernhard Schommer's avatar
      Use library function. · 127b00c5
      Bernhard Schommer authored
      The function String.uppercase was deprecated and the replacement
      function String.upercase_ascii was only available from OCaml 4.03.0.
      Since the minimal OCaml version is now 4.05.0 we can use the function
    • Bernhard Schommer's avatar
      Use Hashtbl.find_opt. · 19aed83c
      Bernhard Schommer authored
      Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None`
      by a call to the function Hashtbl.find_opt.
  13. 25 Jun, 2020 2 commits
    • Xavier Leroy's avatar
      Eliminate known builtins whose result is ignored · 7fe7aabe
      Xavier Leroy authored
      A typical example is `(void) __builtin_sel(a, b, c)`.
      It is safe to generate zero code for these uses of builtins
      because builtins whose semantics are known to the compiler
      are pure.  Other builtins with side effects (e.g. `__builtin_trap`)
      are not known and will remain in the compiled code.
      It is useful to generate zero code for these uses of builtins
      because some of them (e.g. `__builtin_sel`) must be transformed
      into proper CminorSel expressions during instruction selection.
      Otherwise, they propagate all the way to ExpandAsm, causing
      a "not implemented" error there.
    • Xavier Leroy's avatar
      Improve printing of builtin function invocations · c6b86fd5
      Xavier Leroy authored
      In particular __builtin_sel.
  14. 21 Jun, 2020 1 commit
    • Xavier Leroy's avatar
      Preliminary support for Coq 8.12 · 5b8578da
      Xavier Leroy authored
      Based on testing with beta-1 release.
      The deprecation warning about the "omega" tactic is ignored while we
      decide when to switch to "lia" instead.