1. 04 Jan, 2022 1 commit
  2. 08 Dec, 2021 2 commits
  3. 07 Dec, 2021 2 commits
  4. 06 Dec, 2021 8 commits
  5. 03 Dec, 2021 1 commit
  6. 01 Dec, 2021 2 commits
  7. 26 Nov, 2021 1 commit
  8. 23 Nov, 2021 2 commits
  9. 19 Nov, 2021 1 commit
  10. 17 Nov, 2021 2 commits
  11. 16 Nov, 2021 4 commits
    • Xavier Leroy's avatar
      First update for release 3.10 · 9c49dafb
      Xavier Leroy authored
    • Xavier Leroy's avatar
      Maps.v: transparency of Node · a29b0c1b
      Xavier Leroy authored
      Add one more `Local Transparent Node` to ensure compatibility with Coq < 8.12
    • Xavier Leroy's avatar
      An improved PTree data structure (#420) · b9dfe18f
      Xavier Leroy authored
      This PR replaces the "PTree" data structure used in lib/Maps.v by the
      canonical binary tries data structure proposed by A. W. Appel and
      described in the paper "Efficient Extensional Binary Tries",
      The new implementation is more memory-efficient and a bit faster,
      resulting in reduced compilation times (-5% on typical C programs, up
      to -10% on very large C functions).
      It also enjoys the extensionality property (two tries mapping equal
      keys to equal data are equal), which simplifies some proofs.
    • Xavier Leroy's avatar
      Revised checks for multi-character constants 'xyz' · 168495d7
      Xavier Leroy authored
      The previous code for elaborating character constants has a small bug:
      the value of a wide character constant consisting of several characters
      was normalized to type `int`, while, statically, it has type `wchar_t`.
      If `wchar_t` is `unsigned short`, for example, the constant `L'ab'`
      would elaborate to 6357090, which is not of type `unsigned short`.
      This commit fixes the bug by normalizing wide character constants to type
      `wchar_t`, regardless of how many characters they contain.
      The previous code was odd in another respect: leading `\0` characters
      in multi-character constants were ignored.  Hence, `'\0bcde'` was accepted
      while `'abcde'` caused a warning.
      This commit implements a more predictable behavior: the number of characters
      in a character literal is limited a priori to
            sizeof(type of result) / sizeof(type of each character)
      So, for non-wide character constants we can typically have up to 4
      characters (sizeof(int) / sizeof(char)), while for wide character
      constants we can only have one character.
      In effect, multiple-character wide character literals are not supported.
      This is allowed by the ISO C99 standard and seems consistent with GCC
      and Clang.
      Finally, a multi-character constant with too many characters was
      reported either as an error (if the computation overflowed the 64-bit
      accumulator) or as a warning (otherwise).  Here, we make this an error
      in all cases.
      GCC and Clang only produce warnings, and truncate the value of the
      character constant, but an error feels safer.
  12. 12 Nov, 2021 1 commit
    • Xavier Leroy's avatar
      Resurrect a warning for bit fields of enum types · 6431b483
      Xavier Leroy authored
      Earlier CompCert versions would warn if a bit field of width N and
      type enum E was too small for the values of the enumeration: whether
      the field is interpreted as a N-bit signed integer or a N-bit unsigned
      integer, some values of the enumeration are not representable.
      This warning was performed in the Bitfields emulation pass, which went
      away during the reimplementation of bit fields within the verified
      part of CompCert.
      In this commit, we resurrect the warning and perform it during the Elab pass.
      In passing, some of the code that elaborates bit fields was moved to a
      separate function "check_bitfield".
  13. 06 Nov, 2021 1 commit
  14. 02 Nov, 2021 4 commits
  15. 29 Oct, 2021 2 commits
  16. 28 Oct, 2021 1 commit
    • Xavier Leroy's avatar
      PPC64: revised generation of rldic* instructions · d194e47a
      Xavier Leroy authored
      In Op.v, the definitions of is_rldl_mask and is_rldr_mask mask were
      - rldl is for [00001111] masks that clear on the left,
        hence start with 1s and finish with 0s;
      - rldr is for [11110000] masks that clear on the right,
        hence start with 0s and finish with 1s.
      In Asmgen.v, the case for masks of the form [00011111100] that can
      generate a rldic instruction was incorrectly detected.
  17. 25 Oct, 2021 1 commit
  18. 20 Oct, 2021 1 commit
  19. 16 Oct, 2021 2 commits
  20. 04 Oct, 2021 1 commit