1. 16 Nov, 2020 1 commit
  2. 14 Nov, 2020 1 commit
  3. 08 Nov, 2020 1 commit
  4. 31 Mar, 2020 2 commits
  5. 05 Feb, 2020 1 commit
  6. 16 Sep, 2019 1 commit
  7. 26 Feb, 2019 1 commit
  8. 25 Feb, 2019 1 commit
  9. 17 Sep, 2018 1 commit
  10. 14 Sep, 2018 1 commit
  11. 12 Sep, 2018 2 commits
  12. 30 May, 2018 3 commits
  13. 13 Jan, 2018 1 commit
  14. 11 Jan, 2018 1 commit
  15. 18 Dec, 2017 1 commit
    • Xavier Leroy's avatar
      Coq 8.7.1 support · 3c23a268
      Xavier Leroy authored
      It is compatible with 8.7.0 and 8.6.1, no changes required to the Coq sources of CompCert.
      3c23a268
  16. 24 Nov, 2017 1 commit
  17. 22 Nov, 2017 1 commit
  18. 20 Oct, 2017 1 commit
    • Xavier Leroy's avatar
      Coq 8.7.0 support · c96c5057
      Xavier Leroy authored
      configure: accept Coq 8.7.0 and 8.6.1.
        (Coq 8.6 became incompatible with commit b4f59c47.)
      Changelog: updated.
      c96c5057
  19. 11 Sep, 2017 1 commit
  20. 22 Aug, 2017 2 commits
  21. 18 Aug, 2017 1 commit
  22. 15 Aug, 2017 1 commit
    • Xavier Leroy's avatar
      Issue #196: excessive proof-checking times in .v files generated by clightgen · ab6d5e98
      Xavier Leroy authored
      The check that "build_composite_env composites = OK (make_composite_env composites)" is taking time exponential on the number of struct/union definitions, at least on the example provided in #196.
      
      The solution implemented in this commit is to use computational reflection more efficiently, just to check that "build_composite_env composites" is of the form "OK _".  From there, a new function Clightdefs.mkprogram produces the appropriate Clight.program without additional computation.
      ab6d5e98
  23. 27 Jul, 2017 1 commit
  24. 05 Jul, 2017 1 commit
  25. 12 Jun, 2017 1 commit
  26. 28 Apr, 2017 3 commits
    • Xavier Leroy's avatar
      Update Changelog with recent changes · f2fe37cc
      Xavier Leroy authored
      f2fe37cc
    • Xavier Leroy's avatar
      RISC-V port and assorted changes · f642817f
      Xavier Leroy authored
      This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes.
      
      The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/
      
      This port required the following additional changes:
      
      - Integers: More properties about shrx
      
      - SelectOp: now provides smart constructors for mulhs and mulhu
      
      - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu.
      
      - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert.  Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library.
      
      - test/: add SIMU make variable to run tests through a simulator
      
      - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers
      
      commit da14495c01cf4f66a928c2feff5c53f09bde837f
      Author: Xavier Leroy <xavier.leroy@inria.fr>
      Date:   Thu Apr 13 17:36:10 2017 +0200
      
          RISC-V port, continued
      
          Now working on Asmgen.
      
      commit 36f36eb3a5abfbb8805960443d087b6a83e86005
      Author: Xavier Leroy <xavier.leroy@inria.fr>
      Date:   Wed Apr 12 17:26:39 2017 +0200
      
          RISC-V port, first steps
      
          This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64).  Work in progress.
      f642817f
    • Xavier Leroy's avatar
  27. 15 Feb, 2017 1 commit
  28. 14 Feb, 2017 1 commit
  29. 10 Feb, 2017 1 commit
  30. 07 Feb, 2017 1 commit
  31. 31 Jan, 2017 1 commit
  32. 27 Oct, 2016 1 commit
  33. 18 Jul, 2016 1 commit