Turn delicate case of designated re-initialization into error (#70)

Consider:
  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.

2 files changed, 6 insertions, 1 deletions

diff --git a/test/regression/Results/initializers3 b/test/regression/Results/initializers3
index 8742f8ea..fb20e5a9 100644
--- a/test/regression/Results/initializers3
+++ b/test/regression/Results/initializers3
@@ -7,5 +7,4 @@ x21 = { 'H', 'e', 'l', 'l', 'o', '!', 0, 0, 0, 0, }
 f(0,42) = 42, f(1,42) = 43, f(2,42) = 44, f(3,42) = 44, f(4,42) = 44
 s1 = { tag = 0, a = {66,77}, u = {0,0} }
 s2 = { tag = 0, a = {0,1}, u = {66,77} }
-s3 = { tag = 1, a = {1,0}, u = {'H', 'e', 'l', 'l', 'o', '!', 0, 'X', } }
 s4 = { tag = 0, a = {66,77}, u = {88,99} }
diff --git a/test/regression/initializers3.c b/test/regression/initializers3.c
index 359a0f71..0769facc 100644
--- a/test/regression/initializers3.c
+++ b/test/regression/initializers3.c
@@ -82,8 +82,14 @@ int main()
   print_S("s1", &s1);
   struct S s2 = { .a.y = 1, .u.c[4] = 'x', .u.b = p1 };
   print_S("s2", &s2);
+  /* ISO C99 and recent Clang say s3.a.y = 77
+     GCC and earlier CompCert versions say s3.a.y = 0
+     Now CompCert fails on an error "unsupported reinitialization". */
+#if 0
   struct S s3 = { .tag = 1, .a = p1, .a.x = 1, .u.c = "Hello!", .u.c[7] = 'X' };
   print_S("s3", &s3);
+#endif
+  /* This other reinitialization is correctly supported, though. */
   struct S s4 = { .tag = 0, .a.x = 1, .a = p1, .u.b = 88, 99 };
   print_S("s4", &s4);
   return 0;