1. 04 Apr, 2018 31 commits
  2. 03 Apr, 2018 1 commit
  3. 30 Mar, 2018 1 commit
    • Xavier Leroy's avatar
      Turn delicate case of designated re-initialization into error (#70) · 1ee8c156
      Xavier Leroy authored
        struct P { int x, y; }
        struct S { struct P p; }
        struct P p0 = { 1,2 };
        struct S s1 = { .p = p0; .p.x = 3 };
      ISO C99 and recent versions of Clang initialize s1.p.y to 2, i.e.
      the initialization of s1.p.y to p0.y implied by ".p = p0" is kept,
      even though the initialization of s1.p.x to p0.x is overwritten
      by ".p.x = 3".
      GCC, old versions of Clang, and previous versions of CompCert
      initialize s1.p.y to the default value 0.  I.e. the initialization
      ".p = p0" is forgotten, leaving default values for the fields of .p
      before ".p.x = 3" takes effect.
      Implementing the proper ISO C99 semantics in CompCert is difficult,
      owing to a mismatch between the intended semantics and the C.init
      representation of initializers.
      This commit turns the delicate case of reinitialization above
      (re-initializing a member of a composite that has already been
      initialized as a whole) into a compile-time error.
      We will then see if the delicate case occurs in practice and needs
      further attention.
  4. 29 Mar, 2018 2 commits
    • Bernhard Schommer's avatar
      Reject casts to struct/union types (#68) · 6b1463c4
      Bernhard Schommer authored
      The ISO C99 standard allows cast only if the type name involved
      is either a void type or a scalar type.  
      For compatibility with GCC and Clang we used to support casting
      a struct or union to exactly the same struct or union type.
      That does not seem useful in practice and complicates conformance
      testing.  This commit gets rid of this exception to the C99 rule.
      Bug 23310
    • Bernhard Schommer's avatar
      Don't overwrite initializer of anonymous union member. (#69) · d1ff2fcb
      Bernhard Schommer authored
      Instead of overwriting the initializer of the anonymous member we
      should just keep it.
      Bug 23353
  5. 28 Mar, 2018 2 commits
    • Bernhard Schommer's avatar
      Fix 23332 · de293458
      Bernhard Schommer authored
    • Jasper Hugunin's avatar
      Change Implicit Arguments to Arguments (#225) · 5e665ecc
      Jasper Hugunin authored
      Implicit Arguments is deprecated in Coq since 8.6 or so.  
      Some Implicit Arguments remained in Flocq but were recently changed to Arguments.  
      Apply the same change to our local copy of Flocq.
      As a positive consequence, we no longer need to suppress the deprecation warnings while compiling Flocq.
  6. 27 Mar, 2018 3 commits