diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-10-05 08:11:34 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-10-05 08:11:34 +0000 |
commit | a6c369cbd63996c1571ae601b7d92070f024b22c (patch) | |
tree | dc4f3f5a52ae4ea230f307ce5f442137f014b79b /cfrontend/Initializers.v | |
parent | b55147379939553eccd4289fd18e7f161619be4d (diff) | |
download | compcert-a6c369cbd63996c1571ae601b7d92070f024b22c.tar.gz compcert-a6c369cbd63996c1571ae601b7d92070f024b22c.zip |
Merge of the "alignas" branch.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2342 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Initializers.v')
-rw-r--r-- | cfrontend/Initializers.v | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v index e7debfcb..ec06cfdb 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 _ => |