aboutsummaryrefslogtreecommitdiffstats
path: root/cparser
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-01-31 14:21:50 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2017-01-31 14:21:50 +0100
commit3581ae495677aeca93f013d67a4d4f7c171d9cc0 (patch)
tree8508b05e2ce313cdb7bd5504805580a655aa9813 /cparser
parent1fe7f0c7ec5e1a4425eb09939d0e8f6143f1f913 (diff)
downloadcompcert-3581ae495677aeca93f013d67a4d4f7c171d9cc0.tar.gz
compcert-3581ae495677aeca93f013d67a4d4f7c171d9cc0.zip
Normalize offset to size_t kind.
Diffstat (limited to 'cparser')
-rw-r--r--cparser/Elab.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index f4f1586c..3dc1816b 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1676,8 +1676,10 @@ let elab_expr vararg loc env a =
env,off_accu + size * (Int64.to_int e),sub_ty
| ATINDEX_INIT _,_ -> error "subscripted value is not an array" in
let env,offset,_ = List.fold_left offset_of_member (env,0,ty) mem in
- let offsetof_const = EConst (CInt(Int64.of_int offset,size_t_ikind (),"")) in
- { edesc = offsetof_const; etyp = TInt(size_t_ikind(), []) },env
+ let size_t = size_t_ikind () in
+ let offset = Ceval.normalize_int (Int64.of_int offset) size_t in
+ let offsetof_const = EConst (CInt(offset,size_t,"")) in
+ { edesc = offsetof_const; etyp = TInt(size_t, []) },env
| UNARY(PLUS, a1) ->
let b1,env = elab env a1 in