diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index 132d30d68c5e67a30f5ee892952e95ba6a38a3c0..dd9c80abda0b4c0838a65ba493617444d1d296c9 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -3635,19 +3635,22 @@ let setReturnTypeVI (v: varinfo) (t: typ) =
 let setReturnType (f:fundec) (t:typ) =
   setReturnTypeVI f.svar t
 
-(** Returns the type pointed by the given type. Asserts it is a pointer type *)
 let typeOf_pointed typ =
   match unrollType typ with
   | TPtr (typ,_) -> typ
   | _ -> Kernel.fatal "Not a pointer type %a" !pp_typ_ref typ
 
-(** Returns the type of the elements of the array. Asserts it is an array type
-*)
 let typeOf_array_elem t =
   match unrollType t with
   | TArray (ty_elem, _, _) -> ty_elem
   | _ -> Kernel.fatal "Not an array type %a" !pp_typ_ref t
 
+let typeOf_array_elem_size t =
+  match unrollType t with
+  | TArray (ty_elem, arr_size, _ ) ->
+    ty_elem, Option.bind arr_size !constfoldtoint
+  | _ -> Kernel.fatal "Not an array type %a" !pp_typ_ref t
+
 let no_op_coerce typ t =
   match typ with
   | Lreal -> isLogicArithmeticType t.term_type
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index cb016440a6ce183d18b3732dd68c6bbf700b15ec..e5a54e543c600d0ba69656229aa16b3632b7e56d 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -1253,6 +1253,12 @@ val typeOf_array_elem : typ -> typ
 (** Returns the type of the array elements of the given type.
     Asserts it is an array type. *)
 
+val typeOf_array_elem_size : typ -> typ * Z.t option
+(** Returns the type of the array elements of the given type, and the size
+    of the array, if any.
+    Asserts it is an array type.
+    @since Frama-C+dev *)
+
 val is_fully_arithmetic: typ -> bool
 (** Returns [true] whenever the type contains only arithmetic types *)
 
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 ac29123b225b9979e8d3ae8f8da320ce756307a4..2ceca06655fada23fd1b4a5925b939e328c98113 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 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 update (m: map) (n: node) (f: chunk -> chunk) =
-  let r = get m n in
-  Ufind.set m.store n (f r)
-
-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
 
 (* -------------------------------------------------------------------------- *)
@@ -254,12 +254,14 @@ let pp_region fmt (m: region) =
     Format.fprintf fmt " ;@]" ;
   end
 
-let make_range (m: map) (rg: rg) : range = {
-  offset = rg.offset ;
-  length = rg.length ;
-  cells = rg.length / sizeof (get m rg.data).clayout ;
-  data = node m rg.data ;
-}
+let make_range (m: map) (rg: rg) : range =
+  let s = sizeof (get m rg.data).clayout in
+  {
+    offset = rg.offset ;
+    length = rg.length ;
+    cells = if s = 0 then 0 else rg.length / s ;
+    data = node m rg.data ;
+  }
 
 let make_region (m: map) (n: node) (r: chunk) : region = {
   node = n ;
@@ -330,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)
@@ -357,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
 
@@ -390,9 +392,9 @@ let merge_all (m:map) = function
       do_merge m q a b ;
     done
 
-let merge (m: map) (a: node) (b: node) : node =
+let merge (m: map) (a: node) (b: node) : unit =
   failwith_locked m "Region.Memory.merge" ;
-  merge_all m [a;b] ; Ufind.find m.store (min a b)
+  merge_all m [a;b]
 
 (* -------------------------------------------------------------------------- *)
 (* --- Offset                                                             --- *)
@@ -403,24 +405,24 @@ 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 s = Cil.bitsSizeOf ty * n in
+  let re = new_chunk m () in
+  let rc = new_range m ~size:s ~offset:0 ~length:s ~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
@@ -430,28 +432,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..2b2f948d436a879d103e927d32a49c54cbb5919c 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
 
@@ -85,7 +84,7 @@ val read : map -> node -> Access.acs -> unit
 val write : map -> node -> Access.acs -> unit
 val shift : map -> node -> Access.acs -> unit
 
-val merge : map -> node -> node -> node
+val merge : map -> node -> node -> unit
 val merge_all : map -> node list -> unit
 
 (** @raise Not_found *)
diff --git a/src/plugins/region/store.ml b/src/plugins/region/store.ml
index 4e964e42b373265fedea995c5665efd92e916e39..a1bd51e505e732b37f1eb85c864e5536ba6abcae 100644
--- a/src/plugins/region/store.ml
+++ b/src/plugins/region/store.ml
@@ -27,18 +27,20 @@
 module Imap = Map.Make(Int)
 
 type 'a rref = int
-type 'a store = 'a Imap.t ref
+type 'a store = {
+  mutable rid : int ;
+  mutable map : 'a Imap.t ;
+}
 
-let new_store () = ref Imap.empty
-let copy r = ref !r
-let rid = ref 0
+let new_store () = { rid = 0 ; map = Imap.empty }
+let copy r = { rid = r.rid ; map = r.map }
 
 let make s v =
-  let k = incr rid ; !rid in
-  s := Imap.add k v !s ; k
+  let k = succ s.rid in
+  s.rid <- k ; s.map <- Imap.add k v s.map ; k
 
-let get s k = Imap.find k !s
-let set s k v = s := Imap.add k v !s
+let get s k = Imap.find k s.map
+let set s k v = s.map <- Imap.add k v s.map
 
 let eq _s i j = (i == j)
 
diff --git a/src/plugins/region/tests/region/blob.i b/src/plugins/region/tests/region/blob.i
new file mode 100644
index 0000000000000000000000000000000000000000..13399b7c3db1b41967612adb0be8dd74c2e25afd
--- /dev/null
+++ b/src/plugins/region/tests/region/blob.i
@@ -0,0 +1,14 @@
+void array_blob() {
+  int arr[3];
+  int* p = &arr[1];
+}
+
+void struct_blob() {
+  struct { int f; char g; } y;
+  int *p = &y.f;
+}
+
+void var_blob() {
+  int x;
+  int* p = &x;
+}
diff --git a/src/plugins/region/tests/region/comp.c b/src/plugins/region/tests/region/comp.c
new file mode 100644
index 0000000000000000000000000000000000000000..ad192b3a2b7cad800184c05b412d7c16ddc9a629
--- /dev/null
+++ b/src/plugins/region/tests/region/comp.c
@@ -0,0 +1,7 @@
+void f() {
+  struct { int x; int y; int* z; short arr[4]; } s;
+  int a = 1;
+  s.x = a;
+  s.z = &a;
+  s.arr[1] = 0;
+}
diff --git a/src/plugins/region/tests/region/oracle/blob.res.oracle b/src/plugins/region/tests/region/oracle/blob.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..7231ade0c087fd04d00f93ec9432404752374529
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/blob.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing blob.i (no preprocessing)
+[region] Analyzing regions
+[region] Function array_blob:
+  R0003: --- arr 96b 0..96 [0]: R0004 ;
+  R0004: --- 0b ;
+  R0001: -W- p (int *) 64b (*R0004) ;
+[region] Function struct_blob:
+  R0003: --- y 64b 0..32 [0]: R0004 ;
+  R0004: --- 0b ;
+  R0001: -W- p (int *) 64b (*R0004) ;
+[region] Function var_blob:
+  R0003: --- x 0b ;
+  R0001: -W- p (int *) 64b (*R0003) ;
diff --git a/src/plugins/region/tests/region/oracle/comp.res.oracle b/src/plugins/region/tests/region/oracle/comp.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..760fd5d9552fcb878dbec0a41fa24cb100aad212
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/comp.res.oracle
@@ -0,0 +1,9 @@
+[kernel] Parsing comp.c (with preprocessing)
+[region] Analyzing regions
+[region] Function f:
+  R0003: --- s 192b 0..32 [1]: R0004 64..128 [1]: R0007 128..192 [1]: R000b ;
+  R0004: -W- (int) 32b ;
+  R0007: -W- (int *) 64b (*R0001) ;
+  R0001: RW- a (int) 32b ;
+  R000b: --- 64b 0..64 [4]: R000d ;
+  R000d: -W- (short) 16b ;
diff --git a/src/plugins/region/tests/region/oracle/swap.res.oracle b/src/plugins/region/tests/region/oracle/swap.res.oracle
index 3117fb686d5ee476901cd95a19ab05fd51194ca0..49268e6ca2960f28c6581ce3f0ccf3cfee88fd9f 100644
--- a/src/plugins/region/tests/region/oracle/swap.res.oracle
+++ b/src/plugins/region/tests/region/oracle/swap.res.oracle
@@ -6,8 +6,8 @@
   R0001: R-- b (int *) 64b (*R0007) ;
   R0008: RW- tmp (int) 32b ;
 [region] Function swap_separated:
-  R0013: R-- a (int *) 64b (*R0016) ;
-  R0016: RW- A: (int) 32b ;
-  R0017: R-- b (int *) 64b (*R001a) ;
-  R001a: RW- B: (int) 32b ;
-  R001b: RW- tmp (int) 32b ;
+  R0001: R-- a (int *) 64b (*R0004) ;
+  R0004: RW- A: (int) 32b ;
+  R0005: R-- b (int *) 64b (*R0008) ;
+  R0008: RW- B: (int) 32b ;
+  R0009: RW- tmp (int) 32b ;