diff --git a/ivette/src/frama-c/plugins/region/api/index.ts b/ivette/src/frama-c/plugins/region/api/index.ts
index 942053971ed63a0baf6086a312b1c24ba5f27e28..a0b2fef89282dafb2469897c389922c546a54e65 100644
--- a/ivette/src/frama-c/plugins/region/api/index.ts
+++ b/ivette/src/frama-c/plugins/region/api/index.ts
@@ -162,14 +162,32 @@ const regions_internal: Server.GetRequest<decl,region[]> = {
 /** Compute regions for the given declaration */
 export const regions: Server.GetRequest<decl,region[]>= regions_internal;
 
-const regionsAt_internal: Server.GetRequest<marker,region[]> = {
+const regionsAt_internal: Server.GetRequest<[ marker, boolean ],region[]> = {
   kind: Server.RqKind.GET,
   name: 'plugins.region.regionsAt',
-  input: jMarker,
+  input: Json.jPair( jMarker, Json.jBoolean,),
   output: Json.jArray(jRegion),
   signals: [ { name: 'plugins.region.updated' } ],
 };
-/** Compute regions at the given marker position */
-export const regionsAt: Server.GetRequest<marker,region[]>= regionsAt_internal;
+/** Compute regions at the given marker */
+export const regionsAt: Server.GetRequest<[ marker, boolean ],region[]>= regionsAt_internal;
+
+const localize_internal: Server.GetRequest<
+  [ marker, boolean ],
+  node |
+  undefined
+  > = {
+  kind: Server.RqKind.GET,
+  name: 'plugins.region.localize',
+  input: Json.jPair( jMarker, Json.jBoolean,),
+  output: Json.jOption(jNode),
+  signals: [ { name: 'plugins.region.updated' } ],
+};
+/** Localize in the local (true) or global map (false) */
+export const localize: Server.GetRequest<
+  [ marker, boolean ],
+  node |
+  undefined
+  >= localize_internal;
 
 /* ------------------------------------- */
diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml
index c7f3e43ccf48d83a5230e7d3103692dbb9a7347b..b0231ead15f8d05cacbde79a00dcfeb7bfe4ae6d 100644
--- a/src/plugins/region/code.ml
+++ b/src/plugins/region/code.ml
@@ -164,10 +164,9 @@ let instr (m:map) (s:stmt) (instr:instr) =
 type rmap = Memory.map Stmt.Map.t ref
 
 let store rmap m s =
-  rmap := Stmt.Map.add s (Memory.copy m) !rmap
+  rmap := Stmt.Map.add s (Memory.copy ~locked:true m) !rmap
 
 let rec stmt (r:rmap) (m:map) (s:stmt) =
-
   let annots = Annotations.code_annot s in
   if annots <> [] then
     Options.warning ~source:(fst @@ Stmt.loc s)
@@ -218,8 +217,8 @@ type domain = {
   spec : map Property.Map.t ;
 }
 
-let domain kf =
-  let m = Memory.create () in
+let domain ?global kf =
+  let m = match global with Some g -> g | None -> Memory.create () in
   let r = ref Stmt.Map.empty in
   begin
     try
@@ -227,7 +226,7 @@ let domain kf =
       block r m fundec.sbody ;
     with Kernel_function.No_Definition -> ()
   end ; {
-    map = m ;
+    map = Memory.copy ~locked:true m ;
     body = !r ;
     spec = Property.Map.empty ;
   }
diff --git a/src/plugins/region/code.mli b/src/plugins/region/code.mli
index 1ae6e52fc2cad0299423705efccb09c2267fc9af..fb4df16f1afa2b3a2f4cc8edd92d689b46a37442 100644
--- a/src/plugins/region/code.mli
+++ b/src/plugins/region/code.mli
@@ -29,10 +29,12 @@ val exp : map -> stmt -> exp -> node option
 val instr : map -> stmt -> instr -> unit
 val stmt : map Stmt.Map.t ref -> map -> stmt -> unit
 
+(** All the provided maps are locked. *)
 type domain = {
   map : map ;
   body : map Stmt.Map.t ;
   spec : map Property.Map.t ;
 }
 
-val domain : kernel_function -> domain
+(** The global map, if provided, is used as an accumulator. *)
+val domain : ?global:map -> kernel_function -> domain
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 2ac7d0d25ef1389b5e17a6bdadfcb2f615070ff8..8ac0519149bef24a9f2ff870c004bebcf7841fae 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -51,6 +51,7 @@ type rg = node Ranges.range
 
 type map = {
   store: chunk Ufind.store ;
+  mutable locked: bool ;
   mutable index: node Vmap.t ;
 }
 
@@ -70,6 +71,12 @@ let types (m : chunk) : typ list =
   Access.Set.iter add m.cwrites ;
   Typ.Set.elements !pool
 
+let failwith_locked m fn =
+  if m.locked then raise (Invalid_argument fn)
+
+let lock m = m.locked <- true
+let unlock m = m.locked <- false
+
 (* -------------------------------------------------------------------------- *)
 (* --- Printers                                                           --- *)
 (* -------------------------------------------------------------------------- *)
@@ -110,11 +117,13 @@ let pp_chunk fmt (n: node) (m: chunk) =
 (* -------------------------------------------------------------------------- *)
 
 let create () = {
+  locked = false ;
   store = Ufind.new_store () ;
   index = Vmap.empty ;
 }
 
-let copy m = {
+let copy ?locked m = {
+  locked = (match locked with None -> m.locked | Some l -> l) ;
   store = Ufind.copy m.store ;
   index = m.index ;
 }
@@ -150,6 +159,7 @@ let get map node =
 (* -------------------------------------------------------------------------- *)
 
 let cell (m: map) ?size ?ptr ?root () =
+  failwith_locked m "Region.Memory.cell" ;
   let clayout = match size, ptr with
     | None, None -> Blob
     | None, Some _ -> Cell(Cil.bitsSizeOf Cil.voidPtrType,ptr)
@@ -162,6 +172,7 @@ let update (m: map) (n: node) (f: chunk -> chunk) =
   Ufind.set m.store n (f r)
 
 let range (m: map) ~size ~offset ~length ~data : node =
+  failwith_locked m "Region.Memory.range" ;
   let last = offset + length in
   if not (0 <= offset && offset < last && last <= size) then
     raise (Invalid_argument "Region.Memory.range") ;
@@ -171,6 +182,7 @@ let range (m: map) ~size ~offset ~length ~data : node =
 
 let root (m: map) v =
   try Vmap.find v m.index with Not_found ->
+    failwith_locked m "Region.Memory.root" ;
     let n = cell m ~root:v () in
     m.index <- Vmap.add v n m.index ; n
 
@@ -262,6 +274,11 @@ let iter (m:map) (f: region -> unit) =
   let h = Hashtbl.create 0 in
   Vmap.iter (fun _x n -> walk h m f n) m.index
 
+let regions map =
+  let pool = ref [] in
+  iter map (fun r -> pool := r :: !pool) ;
+  List.rev !pool
+
 (* -------------------------------------------------------------------------- *)
 (* --- Merge                                                              --- *)
 (* -------------------------------------------------------------------------- *)
@@ -344,6 +361,7 @@ let do_merge (m: map) (q: queue) (a: node) (b: node): unit =
   end
 
 let merge (m: map) (a: node) (b: node) : node =
+  failwith_locked m "Region.Memory.merge" ;
   if Ufind.eq m.store a b then Ufind.find m.store a else
     let q = Queue.create () in
     do_merge m q a b ;
@@ -363,21 +381,80 @@ let access (m:map) (a:node) (ty: typ) =
   if sr <> size then ignore (merge m a (cell m ~size ()))
 
 let points_to (m: map) (a: node) (b : node) =
+  failwith_locked m "Region.Memory.points_to" ;
   ignore @@ merge m a @@ cell m ~ptr:b ()
 
 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)
 
 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)
 
 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 *)
 
 (* -------------------------------------------------------------------------- *)
+(* --- Lookup                                                            ---- *)
+(* -------------------------------------------------------------------------- *)
+
+let cranges m r =
+  let rg = Ufind.get m.store r in
+  match rg.clayout with
+  | Blob | Cell _ -> raise Not_found
+  | Compound(s,rgs) -> s, rgs
+
+let cpointed m r =
+  let rg = Ufind.get m.store r in
+  match rg.clayout with
+  | Blob | Compound _ | Cell(_,None) -> None
+  | Cell(_,Some r) -> Some (Ufind.find m.store r)
+
+let rec lval (m: map) (lv: lval) : node =
+  let h = host m (fst lv) in
+  offset m h (snd lv)
+
+and host (m: map) (h: lhost) : node =
+  match h with
+  | Var x -> Ufind.find m.store @@ Vmap.find x m.index
+  | Mem e ->
+    match exp m e with
+    | None -> raise Not_found
+    | Some r -> r
+
+and offset (m: map) (r: node) (ofs: offset) : node =
+  match ofs with
+  | NoOffset -> Ufind.find m.store r
+  | Field (fd, ofs) ->
+    let _, rgs = cranges m r in
+    let (p,w) = Cil.fieldBitsOffset fd in
+    let rg = Ranges.find p rgs in
+    if rg.offset <= p && p+w <= rg.offset + rg.length then
+      offset m rg.data ofs
+    else raise Not_found
+  | Index (_, ofs) ->
+    let s, rgs = cranges m r in
+    match rgs with
+    | R [rg] when rg.offset = 0 && rg.length = s ->
+      offset m rg.data ofs
+    | _ -> raise Not_found
+
+and exp (m: map) (e: exp) : node option =
+  match e.enode with
+  | Const _
+  | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ -> None
+  | Lval lv -> cpointed m @@ lval m lv
+  | AddrOf lv | StartOf lv -> Some (lval m lv)
+  | CastE(_, e) -> exp m e
+  | BinOp((PlusPI|MinusPI),p,_,_) -> exp m p
+  | UnOp (_, _, _) | BinOp (_, _, _, _) -> None
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index f1a3bc95e8c0ce8470f529b8f3dce2005289655c..d31f9bcfa71aaca892d8f20d121d5691e10d4305 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -50,8 +50,17 @@ val pp_node : Format.formatter -> node -> unit
 val pp_range : Format.formatter -> range -> unit
 val pp_region : Format.formatter -> region -> unit
 
+(** Initially unlocked. *)
 val create : unit -> map
-val copy : map -> map
+
+(** Default locked status is inherited from the copied map. *)
+val copy : ?locked:bool -> map -> map
+
+(** Lock the map. No more access nor merge can be added into the map. *)
+val lock : map -> unit
+
+(** Unlock the map. *)
+val unlock : map -> unit
 
 val root : map -> Cil_types.varinfo -> node
 val cell : map -> ?size:int -> ?ptr:node -> ?root:varinfo -> unit -> node
@@ -61,11 +70,19 @@ val id : node -> int
 val forge : int -> node
 val node : map -> node -> node
 val nodes : map -> node list -> node list
-val region : map -> node -> region
+
 val iter : map -> (region -> unit) -> unit
+val region : map -> node -> region
+val regions : map -> region list
 
 val merge : map -> node -> node -> node
 val read : map -> node -> Access.acs -> unit
 val write : map -> node -> Access.acs -> unit
 val shift : map -> node -> Access.acs -> unit
 val points_to : map -> node -> node -> unit
+
+(** @raise Not_found *)
+val lval : map -> lval -> node
+
+(** @raise Not_found *)
+val exp : map -> exp -> node option
diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml
index 38550cc6615d9f10c3a59337a2274af002c242bf..d92e5850987d719e45010172f9f6795cf63aaf22 100644
--- a/src/plugins/region/services.ml
+++ b/src/plugins/region/services.ml
@@ -176,20 +176,27 @@ module Regions = Data.Jlist(Region)
 (* --- Server API                                                         --- *)
 (* -------------------------------------------------------------------------- *)
 
-let regions map =
-  let pool = ref [] in
-  Memory.iter map (fun r -> pool := r :: !pool) ;
-  List.rev !pool
-
-let map_of_localizable (loc : Printer_tag.localizable) =
+let map_of_localizable ~local (loc : Printer_tag.localizable) =
   let open Printer_tag in
   match kf_of_localizable loc with
   | None -> raise Not_found
   | Some kf ->
     let domain = Analysis.find kf in
-    match ki_of_localizable loc with
-    | Kglobal -> domain.map
-    | Kstmt s -> Stmt.Map.find s domain.body
+    if local then
+      match ki_of_localizable loc with
+      | Kglobal -> domain.map
+      | Kstmt s -> Stmt.Map.find s domain.body
+    else domain.map
+
+let region_of_localizable (m: Memory.map) (loc: Printer_tag.localizable) =
+  try
+    match loc with
+    | PExp(_,_,e) -> Memory.exp m e
+    | PLval(_,_,lv) -> Some (Memory.lval m lv)
+    | PVDecl(_,_,x) -> Some (Memory.lval m (Var x,NoOffset))
+    | PStmt _ | PStmtStart _
+    | PTermLval _ | PGlobal _ | PIP _ | PType _ -> None
+  with Not_found -> None
 
 let map_of_declaration (decl : Printer_tag.declaration) =
   match decl with
@@ -217,20 +224,34 @@ let () =
     ~output:(module Regions)
     ~signals:[signal]
     begin fun decl ->
-      try regions @@ map_of_declaration decl
+      try Memory.regions @@ map_of_declaration decl
       with Not_found -> []
     end
 
 let () =
   Request.register
     ~package ~kind:`GET ~name:"regionsAt"
-    ~descr:(Md.plain "Compute regions at the given marker position")
-    ~input:(module Kernel_ast.Marker)
+    ~descr:(Md.plain "Compute regions at the given marker")
+    ~input:(module Data.Jpair(Kernel_ast.Marker)(Data.Jbool))
     ~output:(module Regions)
     ~signals:[signal]
-    begin fun loc ->
-      try regions @@ map_of_localizable loc
+    begin fun (loc,local) ->
+      try Memory.regions @@ map_of_localizable ~local loc
       with Not_found -> []
     end
 
+let () =
+  Request.register
+    ~package ~kind:`GET ~name:"localize"
+    ~descr:(Md.plain "Localize in the local (true) or global map (false)")
+    ~input:(module Data.Jpair(Kernel_ast.Marker)(Data.Jbool))
+    ~output:(module NodeOpt)
+    ~signals:[signal]
+    begin fun (loc,local) ->
+      try
+        let map = map_of_localizable ~local loc in
+        region_of_localizable map loc
+      with Not_found -> None
+    end
+
 (* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/services.mli b/src/plugins/region/services.mli
index d694a69647e25710b990a406e84de4142d73b297..2507b13f97d60fac6b22584dd12c0d4bac2f15e5 100644
--- a/src/plugins/region/services.mli
+++ b/src/plugins/region/services.mli
@@ -28,6 +28,3 @@ val package : Package.package
 module Node : Data.S with type t = Memory.node
 module Range : Output with type t = Memory.range
 module Region : Output with type t = Memory.region
-
-(** @raises Not_found *)
-val map_of_localizable : Printer_tag.localizable -> Memory.map