Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

  1. 01 Jun, 2021 2 commits
  2. 08 May, 2021 1 commit
  3. 13 Apr, 2021 1 commit
  4. 18 Jan, 2021 1 commit
    • Xavier Leroy's avatar
      "macosx" is now called "macos" · ab62e1be
      Xavier Leroy authored
      The configure script still accepts "macosx" for backward compatibility,
      but every other part of CompCert now uses "macos".
      ab62e1be
  5. 26 Dec, 2020 1 commit
    • Xavier Leroy's avatar
      AArch64: macOS port · c50680bb
      Xavier Leroy authored
      This commit adds support for macOS (and probably iOS) running on
      AArch64 / ARM 64-bit / "Apple silicon" processors.
      c50680bb
  6. 15 Dec, 2020 1 commit
  7. 26 May, 2020 1 commit
  8. 14 Oct, 2019 1 commit
  9. 20 Sep, 2019 1 commit
  10. 19 Sep, 2019 1 commit
  11. 08 Aug, 2019 1 commit
    • Xavier Leroy's avatar
      AArch64 port · 7cdd676d
      Xavier Leroy authored
      This commit adds a back-end for the AArch64 architecture, namely ARMv8
      in 64-bit mode.
      7cdd676d
  12. 30 Jan, 2019 1 commit
  13. 20 Aug, 2018 1 commit
    • Bernhard Schommer's avatar
      Add sizeof_reg and new Machine configurations (#129) · 6fc89e5c
      Bernhard Schommer authored
      Since the size of integer registers is not identical to the size of pointers
      for the ppc64 and e5500 model the check for register pairs in
      ExtendedAsm does not work correctly.
      
      In order to avoid this a new field sizeof_intreg is introduced in the
      Machine configuration which describes the size of integer registers.
      New configurations for the ppc64 and e5500 model are added
      and used.
      
      Bug 24273
      6fc89e5c
  14. 26 Apr, 2018 1 commit
  15. 04 Apr, 2018 1 commit
  16. 19 Feb, 2018 1 commit
  17. 16 Feb, 2018 1 commit
  18. 22 Aug, 2017 1 commit
  19. 28 Apr, 2017 1 commit
    • 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
  20. 05 Aug, 2016 1 commit
    • Bernhard Schommer's avatar
      Implement support for big endian arm targets. · 028aaefc
      Bernhard Schommer authored
      Adds support for the big endian arm targets by making the target
      endianess flag configurable, adding support for the big endian
      calling conventions, rewriting memory access patterns and adding
      big endian versions of the runtime functions.
      Bug 19418
      028aaefc
  21. 07 Jul, 2015 1 commit
  22. 20 Mar, 2015 1 commit
  23. 14 Mar, 2015 1 commit
    • Xavier Leroy's avatar
      Improve performance and configurability for the StructReturn pass. · 67e8b783
      Xavier Leroy authored
      configure: special ABI value for IA32/MacOSX and PowerPC/Linux
      cparser/Machine: special config for PowerPC/Linux
      cparser/StructReturn: generate better code for return-as-int
      driver/Clflags, driver/Driver: add options -fstruct-return=<convention>
        and -fstruct-passing=<convention> to simplify testing
      67e8b783
  24. 27 Jan, 2015 1 commit
    • Xavier Leroy's avatar
      ABI compatibility for struct/union function arguments passed by value. · e096fa7a
      Xavier Leroy authored
      The passing of struct/union arguments by value implemented in the verified
      part of CompCert is not compatible with the ARM, PowerPC and x86 ABI.
      Here we enrich the StructReturn source-to-source emulation pass
      so that it implements the calling conventions defined in these ABIs.
      
      Plus: for x86, implement the returning of struct/union results by value
      in a way compatible with the ABI.
      e096fa7a
  25. 22 Jan, 2015 1 commit
    • Xavier Leroy's avatar
      Delay reads from !Machine.config before it is properly initialized. · 1e97bb4f
      Xavier Leroy authored
      Several definitions in Cutil and elsewhere were accessing the default
      value of !Machine.config, before it is properly initialized in Driver.
      Delay evaluation of these definitions, and initialize Machine.config
      to nonsensical values so that lack of initialization is caught early
      (e.g. in Cutil.find_matching_*_kind).
      
      Also, following up on commit [3b8a094d], don't use "wchar_t" typedef
      to type wide string literals, even if this typedef is in scope.
      The risk here is to hide an inconsistency between "wchar_t"'s definition
      in standard headers and CompCert's built-in definition.
      1e97bb4f
  26. 30 Dec, 2014 1 commit
    • Xavier Leroy's avatar
      PR#6: fix handling of wchar_t and assignments from wide string literals. · 3b8a094d
      Xavier Leroy authored
      - cparser/Machine indicates whether wchar_t is signed or not
        (it is signed int in Linux and BSD, but unsigned short in Win32)
      - The type of a wide string literal is "wchar_t *" if the typedef "wchar_t"
        exists in the environment (e.g. after #include <stddef.h>).  Only if
        wchar_t is not defined do we use the default from Machine.
      - Permit initialization of any integer array from a wide string literal,
        not just an array of wchar_t.
      3b8a094d
  27. 12 Jan, 2014 1 commit
  28. 20 Dec, 2013 1 commit
  29. 29 Apr, 2013 1 commit
  30. 26 Nov, 2011 1 commit
  31. 10 Mar, 2011 1 commit
  32. 03 Mar, 2010 1 commit