From c677f108ff340c5bca67b428aa6e56b47f62da8c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 28 Mar 2014 08:20:14 +0000
Subject: C: Support array initializers that are too short + default init for
 remainder. Elab: Handle C99 designated initializers. C2C, Initializers: more
 precise intermediate AST for initializers.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2439 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Initializers.v | 26 +++++++++-----------------
 1 file changed, 9 insertions(+), 17 deletions(-)

(limited to 'cfrontend/Initializers.v')

diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index f180f980..4054f6e1 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -136,7 +136,9 @@ Fixpoint constval (a: expr) : res val :=
 
 Inductive initializer :=
   | Init_single (a: expr)
-  | Init_compound (il: initializer_list)
+  | Init_array (il: initializer_list)
+  | Init_struct (il: initializer_list)
+  | Init_union (f: ident) (i: initializer)
 with initializer_list :=
   | Init_nil
   | Init_cons (i: initializer) (il: initializer_list).
@@ -174,14 +176,14 @@ Fixpoint transl_init (ty: type) (i: initializer)
   match i, ty with
   | Init_single a, _ =>
       do d <- transl_init_single ty a; OK (d :: nil)
-  | Init_compound il, Tarray tyelt nelt _ =>
+  | Init_array il, Tarray tyelt nelt _ =>
       transl_init_array tyelt il (Zmax 0 nelt)
-  | Init_compound il, Tstruct id fl _ =>
+  | Init_struct il, Tstruct id fl _ =>
       transl_init_struct id ty fl il 0
-  | Init_compound il, Tunion _ Fnil _ =>
-      OK (Init_space (sizeof ty) :: nil)
-  | Init_compound il, Tunion id (Fcons _ ty1 _) _ =>
-      transl_init_union id ty ty1 il
+  | Init_union f i1, Tunion id fl _ =>
+      do ty1 <- field_type f fl;
+      do d <- transl_init ty1 i1;
+      OK (d ++ padding (sizeof ty1) (sizeof ty))
   | _, _ =>
       Error (msg "wrong type for compound initializer")
   end
@@ -212,16 +214,6 @@ with transl_init_struct (id: ident) (ty: type)
       OK (padding pos pos1 ++ d1 ++ d2)
   | _, _ =>
       Error (msg "wrong number of elements in struct initializer")
-  end
-
-with transl_init_union (id: ident) (ty ty1: type) (il: initializer_list)
-                       {struct il} : res (list init_data) :=
-  match il with
-  | Init_nil =>
-      Error (msg "empty union initializer")
-  | Init_cons i1 _ =>
-      do d <- transl_init ty1 i1;
-      OK (d ++ padding (sizeof ty1) (sizeof ty))
   end.
 
 
-- 
cgit