From a6c369cbd63996c1571ae601b7d92070f024b22c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 5 Oct 2013 08:11:34 +0000
Subject: Merge of the "alignas" branch.

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

(limited to 'cfrontend/Initializers.v')

diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index e7debfc..ec06cfd 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -19,6 +19,7 @@ Require Import Floats.
 Require Import Values.
 Require Import AST.
 Require Import Memory.
+Require Import Globalenvs.
 Require Import Ctypes.
 Require Import Cop.
 Require Import Csyntax.
@@ -173,11 +174,15 @@ Fixpoint transl_init (ty: type) (i: initializer)
                      {struct i} : res (list init_data) :=
   match i, ty with
   | Init_single a, _ =>
-      do d <- transl_init_single ty a; OK (d :: nil)
+      do d <- transl_init_single ty a; 
+      OK (d :: padding (Genv.init_data_size d) (sizeof ty))
   | Init_compound il, Tarray tyelt sz _ =>
-      if zle sz 0
-      then OK (Init_space(sizeof tyelt) :: nil)
-      else transl_init_array tyelt il sz
+      if zle sz 0 then
+        OK (Init_space(sizeof ty) :: nil)
+      else
+        do dl <- transl_init_array tyelt il sz;
+        OK(let n := sizeof ty - sizeof tyelt * sz in
+           if zle n 0 then dl else dl ++ Init_space n :: nil)
   | Init_compound il, Tstruct _ Fnil _ =>
       OK (Init_space (sizeof ty) :: nil)
   | Init_compound il, Tstruct id fl _ =>
-- 
cgit v1.2.3