diff --git a/src/plugins/region/annot.ml b/src/plugins/region/annot.ml
index 825ebf5ce8f52c2fd19a66e55adf11ef979814a4..18c7a9e181f48b0e5ff06bce815f0bddc69346b8 100644
--- a/src/plugins/region/annot.ml
+++ b/src/plugins/region/annot.ml
@@ -38,8 +38,8 @@ and step =
   | Var of varinfo
   | AddrOf of path
   | Star of path
-  | Index of path
   | Shift of path
+  | Index of path * int
   | Field of path * fieldinfo
   | Cast of typ * path
 
@@ -59,7 +59,7 @@ let atomic = function
 let rec pp_step fmt = function
   | Var x -> Varinfo.pretty fmt x
   | Field(p,f) -> pfield p f fmt
-  | Index a -> Format.fprintf fmt "%a[..]" pp_atom a
+  | Index(a,n) -> Format.fprintf fmt "%a[%d]" pp_atom a n
   | Shift a -> Format.fprintf fmt "%a+(..)" pp_atom a
   | Star a -> Format.fprintf fmt "*%a" pp_atom a
   | AddrOf a -> Format.fprintf fmt "&%a" pp_atom a
@@ -184,8 +184,8 @@ let rec parse_lpath (env:env) (e: lexpr) =
       { loc ; step = Star ls ; typ = pointed }
     else
     if Cil.isArrayType typ then
-      let elt = Cil.typeOf_array_elem typ in
-      { loc ; step = Index lv ; typ = elt }
+      let elt,size = Cil.typeOf_array_elem_size typ in
+      { loc ; step = Index(lv,Z.to_int @@ Option.get size) ; typ = elt }
     else
       error env ~loc:lv.loc "Pointer or array type expected"
   | PLcast( t , a ) ->
diff --git a/src/plugins/region/annot.mli b/src/plugins/region/annot.mli
index a2fd8bc531f698f97515c6d863fe5b3ba2f241ee..1fd59bedb1eca8c40bb3a2c77afda316e3b57c1f 100644
--- a/src/plugins/region/annot.mli
+++ b/src/plugins/region/annot.mli
@@ -32,8 +32,8 @@ and step =
   | Var of varinfo
   | AddrOf of path
   | Star of path
-  | Index of path
   | Shift of path
+  | Index of path * int
   | Field of path * fieldinfo
   | Cast of typ * path
 
diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml
index 93bbc497df42f1f637b9fd2c72e4fcc29719c54a..084809d43bd2e06bce04f8841270269b391f166a 100644
--- a/src/plugins/region/code.ml
+++ b/src/plugins/region/code.ml
@@ -34,7 +34,7 @@ let pointer m v =
   match v.ptr with
   | Some p -> v, p
   | None ->
-    let p = add_cell m () in
+    let p = new_chunk m () in
     Option.iter (fun s -> Memory.add_points_to m s p) v.from ;
     { v with ptr = Some p }, p
 
@@ -51,7 +51,9 @@ and add_loffset (m:map) (s:stmt) (r:node) (ty:typ)= function
   | Field(fd,ofs) ->
     add_loffset m s (add_field m r fd) fd.ftype ofs
   | Index(_,ofs) ->
-    add_loffset m s (add_index m r ty) (Cil.typeOf_array_elem ty) ofs
+    let elt,size = Cil.typeOf_array_elem_size ty in
+    let n = Z.to_int @@ Option.get size in
+    add_loffset m s (add_index m r elt n) elt ofs
 
 and add_value m s e = ignore (add_exp m s e)
 
diff --git a/src/plugins/region/logic.ml b/src/plugins/region/logic.ml
index 6e68710a47566de2ab8c01fb50d348c2365e3707..df43142c587fe4fae7664f149f2545712005c2b0 100644
--- a/src/plugins/region/logic.ml
+++ b/src/plugins/region/logic.ml
@@ -27,15 +27,15 @@ let rec add_lval (m:map) (p:path): node =
   match p.step with
   | Var x -> add_root m x
   | Field(lv,fd) -> Memory.add_field m (add_lval m lv) fd
-  | Index lv -> Memory.add_index m (add_lval m lv) lv.typ
+  | Index(lv,n) -> Memory.add_index m (add_lval m lv) lv.typ n
   | Star e | Cast(_,e) -> add_pointer m e
   | Shift _ | AddrOf _ ->
     Options.error ~source:(fst p.loc)
       "Unexpected expression (l-value expected)" ;
-    Memory.add_cell m ()
+    Memory.new_chunk m ()
 and add_pointer  (m:map) (p:path): Memory.node =
   match add_exp m p with
-  | None -> add_cell m ()
+  | None -> Memory.new_chunk m ()
   | Some r -> r
 
 and add_exp (m:map) (p:path): Memory.node option =
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 64b16142b8fdea774edd4adb45caa542f1a9477d..d221fd517741f9377c8f48a1bf949cf0227cea91 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -163,26 +163,24 @@ let get map node =
   try Ufind.get map.store node
   with Not_found -> empty
 
+let update (m: map) (n: node) (f: chunk -> chunk) =
+  let r = get m n in
+  Ufind.set m.store n (f r)
+
 (* -------------------------------------------------------------------------- *)
 (* --- Chunk Constructors                                                 --- *)
 (* -------------------------------------------------------------------------- *)
 
-let add_cell (m: map) ?size ?ptr ?root ?label () =
-  failwith_locked m "Region.Memory.add_cell" ;
-  let clayout = match size, ptr with
-    | None, None -> Blob
-    | None, Some _ -> Cell(Cil.bitsSizeOf Cil.voidPtrType,ptr)
-    | Some s, _ -> Cell(s,ptr) in
-  let croots = Vset.(match root with None -> empty | Some v -> singleton v) in
-  let clabels = Lset.(match label with None -> empty | Some a -> singleton a) in
-  Ufind.make m.store { empty with clayout ; croots ; clabels }
-
-let update (m: map) (n: node) (f: chunk -> chunk) =
-  let r = get m n in
-  Ufind.set m.store n (f r)
+let new_chunk (m: map) ?(size=0) ?ptr () =
+  failwith_locked m "Region.Memory.new_chunk" ;
+  let clayout =
+    match ptr with
+    | None -> if size = 0 then Blob else Cell(size,None)
+    | Some _ -> Cell(Ranges.gcd size Cil.(bitsSizeOf voidPtrType), ptr)
+  in Ufind.make m.store { empty with clayout }
 
-let add_range (m: map) ~size ~offset ~length ~data : node =
-  failwith_locked m "Region.Memory.add_range" ;
+let new_range (m: map) ~size ~offset ~length ~data : node =
+  failwith_locked m "Region.Memory.new_range" ;
   let last = offset + length in
   if not (0 <= offset && offset < last && last <= size) then
     raise (Invalid_argument "Region.Memory.add_range") ;
@@ -193,13 +191,15 @@ let add_range (m: map) ~size ~offset ~length ~data : node =
 let add_root (m: map) v =
   try Vmap.find v m.roots with Not_found ->
     failwith_locked m "Region.Memory.add_root" ;
-    let n = add_cell m ~root:v () in
+    let n = new_chunk m () in
+    update m n (fun d -> { d with croots = Vset.singleton v }) ;
     m.roots <- Vmap.add v n m.roots ; n
 
 let add_label (m: map) a =
   try Lmap.find a m.labels with Not_found ->
     failwith_locked m "Region.Memory.add_label" ;
-    let n = add_cell m ~label:a () in
+    let n = new_chunk m () in
+    update m n (fun d -> { d with clabels = Lset.singleton a }) ;
     m.labels <- Lmap.add a n m.labels ; n
 
 (* -------------------------------------------------------------------------- *)
@@ -332,7 +332,7 @@ let merge_range (m: map) (q: queue) (ra : rg) (rb : rg) : node =
   let size = Ranges.(sa %. sb %. dp %. dq) in
   let data = merge_node m q na nb in
   if size = sa && size = sb then data else
-    merge_node m q (add_cell m ~size ()) data
+    merge_node m q (new_chunk m ~size ()) data
 
 let merge_ranges (m: map) (q: queue)
     (sa : int) (wa : node Ranges.t)
@@ -359,7 +359,7 @@ let merge_layout (m: map) (q: queue) (a : layout) (b : layout) : layout =
     Compound(size, singleton ~size @@ Ranges.squash (merge_node m q) wr)
 
   | Compound(sr,wr), Cell(sx,Some ptr) | Cell(sx,Some ptr), Compound(sr,wr) ->
-    let rp = add_cell m ~size:sx ~ptr () in
+    let rp = new_chunk m ~size:sx ~ptr () in
     let wx = Ranges.range ~length:sx rp in
     merge_ranges m q sx wx sr wr
 
@@ -405,24 +405,25 @@ let add_field (m:map) (r:node) (fd:fieldinfo) : node =
   if ci.cstruct then
     let size = Cil.bitsSizeOf (TComp(ci,[])) in
     let offset, length = Cil.fieldBitsOffset fd in
-    let data = add_cell m () in
-    let rc = add_range m ~size ~offset ~length ~data in
-    ignore @@ merge m r rc ; data
+    let rf = new_chunk m () in
+    let rc = new_range m ~size ~offset ~length ~data:rf in
+    ignore @@ merge m r rc ; rf
   else r
 
-let add_index (m:map) (r:node) (ty:typ) : node =
-  let size = Cil.bitsSizeOf ty in
-  let data = add_cell m () in
-  let rc = add_range m ~size ~offset:0 ~length:size ~data in
-  ignore @@ merge m r rc ; data
+let add_index (m:map) (r:node) (ty:typ) (n:int) : node =
+  let sizelt = Cil.bitsSizeOf ty in
+  let length = sizelt * n in
+  let re = new_chunk m () in
+  let rc = new_range m ~size:length ~offset:0 ~length ~data:re in
+  ignore @@ merge m r rc ; re
 
 let add_points_to (m: map) (a: node) (b : node) =
   failwith_locked m "Region.Memory.points_to" ;
-  ignore @@ merge m a @@ add_cell m ~ptr:b ()
+  ignore @@ merge m a @@ new_chunk m ~ptr:b ()
 
 let add_value (m:map) (rv:node) (ty:typ) : node option =
   if Cil.isPointerType ty then
-    let rp = add_cell m () in
+    let rp = new_chunk m () in
     add_points_to m rv rp ;
     Some rp
   else
@@ -432,28 +433,28 @@ let add_value (m:map) (rv:node) (ty:typ) : node option =
 (* --- Access                                                             --- *)
 (* -------------------------------------------------------------------------- *)
 
-let access (m:map) (a:node) (ty: typ) =
+let sized (m:map) (a:node) (ty: typ) =
   let sr = sizeof (get m a).clayout in
   let size = Ranges.gcd sr (Cil.bitsSizeOf ty) in
-  if sr <> size then ignore (merge m a (add_cell m ~size ()))
+  if sr <> size then ignore (merge m a (new_chunk m ~size ()))
 
 let read (m: map) (a: node) from =
   failwith_locked m "Region.Memory.read" ;
   let r = get m a in
   Ufind.set m.store a { r with creads = Access.Set.add from r.creads } ;
-  access m a (Access.typeof from)
+  sized m a (Access.typeof from)
 
 let write (m: map) (a: node) from =
   failwith_locked m "Region.Memory.write" ;
   let r = get m a in
   Ufind.set m.store a { r with cwrites = Access.Set.add from r.cwrites } ;
-  access m a (Access.typeof from)
+  sized m a (Access.typeof from)
 
 let shift (m: map) (a: node) from =
   failwith_locked m "Region.Memory.shift" ;
   let r = get m a in
-  Ufind.set m.store a { r with cshifts = Access.Set.add from r.cshifts }
-(* no access *)
+  Ufind.set m.store a { r with cshifts = Access.Set.add from r.cshifts } ;
+  sized m a (Access.typeof from)
 
 (* -------------------------------------------------------------------------- *)
 (* --- Lookup                                                            ---- *)
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index 79a0543ef0d220ca2a4da29b4be20a8f570f899d..8fce93bf595b2df31ae2c29b5a01c7f842aad6c7 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -72,12 +72,11 @@ val iter : map -> (region -> unit) -> unit
 val region : map -> node -> region
 val regions : map -> region list
 
+val new_chunk : map -> ?size:int -> ?ptr:node -> unit -> node
 val add_root : map -> Cil_types.varinfo -> node
 val add_label : map -> string -> node
-val add_cell : map -> ?size:int -> ?ptr:node -> ?root:varinfo -> ?label:string -> unit -> node
-val add_range : map -> size:int -> offset:int -> length:int -> data:node -> node
 val add_field : map -> node -> fieldinfo -> node
-val add_index : map -> node -> typ -> node
+val add_index : map -> node -> typ -> int -> node
 val add_points_to : map -> node -> node -> unit
 val add_value : map -> node -> typ -> node option