diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 36fec2b95781966600bf4d0f6fe2fae24c306611..96c787e5500b29aa8f969852bf4817237228e3eb 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -108,14 +108,7 @@ let describe s =
 let validity x =
   if RefUsage.is_nullable x then MemoryContext.Nullable else Valid
 
-module type Proxy = sig
-  val datatype : string
-  val param : Cil_types.varinfo -> MemoryContext.param
-  val iter : ?kf:Kernel_function.t -> init:bool ->
-    (Cil_types.varinfo -> unit) -> unit
-end
-
-module MakeVarUsage(V : Proxy) : MemVar.VarUsage =
+module MakeVarUsage(V : MemVar.VarUsage) : MemVar.VarUsage =
 struct
   let datatype = "VarUsage." ^ V.datatype
 
@@ -141,31 +134,6 @@ end
 (* --- Static Proxy (no preliminary analysis)                             --- *)
 (* -------------------------------------------------------------------------- *)
 
-module Raw : Proxy =
-struct
-  let datatype = "Raw"
-  let param _x = MemoryContext.ByValue
-  (* if x.vaddrof then Separation.InHeap else Separation.ByValue *)
-  let iter ?kf ~init f =
-    begin
-      ignore init ;
-      Globals.Vars.iter (fun x _initinfo -> f x) ;
-      match kf with
-      | None -> ()
-      | Some kf -> List.iter f (Kernel_function.get_formals kf) ;
-    end
-end
-
-module Static : Proxy =
-struct
-  let datatype = "Static"
-  let param x =
-    let open Cil_types in
-    if x.vaddrof || Cil.isArrayType x.vtype || Cil.isPointerType x.vtype
-    then MemoryContext.ByAddr else MemoryContext.ByValue
-  let iter = Raw.iter
-end
-
 (* -------------------------------------------------------------------------- *)
 (* --- RefUsage-based Proxies                                             --- *)
 (* -------------------------------------------------------------------------- *)
@@ -203,21 +171,21 @@ let refusage_param ~byref ~context x =
 
 let refusage_iter ?kf ~init f = RefUsage.iter ?kf ~init (fun x _usage -> f x)
 
-module Var : Proxy =
+module Var : MemVar.VarUsage =
 struct
   let datatype = "Var"
   let param = refusage_param ~byref:false ~context:false
   let iter = refusage_iter
 end
 
-module Ref : Proxy =
+module Ref : MemVar.VarUsage =
 struct
   let datatype = "Ref"
   let param = refusage_param ~byref:true ~context:false
   let iter = refusage_iter
 end
 
-module Caveat : Proxy =
+module Caveat : MemVar.VarUsage =
 struct
   let datatype = "Caveat"
   let param = refusage_param ~byref:true ~context:true
@@ -231,9 +199,10 @@ end
 (* Each model must be instanciated statically because of registered memory
    models identifiers and Frama-C states *)
 
-module Register(V : Proxy)(M : Sigs.Model) = MemVar.Make(MakeVarUsage(V))(M)
+module Register(V : MemVar.VarUsage)(M : Sigs.Model)
+  = MemVar.Make(MakeVarUsage(V))(M)
 
-module Model_Hoare_Raw = Register(Raw)(MemEmpty)
+module Model_Hoare_Raw = Register(MemVar.Raw)(MemEmpty)
 module Model_Hoare_Ref = Register(Ref)(MemEmpty)
 module Model_Typed_Var = Register(Var)(MemTyped)
 module Model_Typed_Ref = Register(Ref)(MemTyped)
@@ -241,14 +210,15 @@ module Model_Caveat = Register(Caveat)(MemTyped)
 
 module MemVal = MemVal.Make(MemVal.Eva)
 
-module MakeCompiler(M:Sigs.Model) = struct
+module MakeCompiler(M:Sigs.Model) =
+struct
   module M = M
   module C = CodeSemantics.Make(M)
   module L = LogicSemantics.Make(M)
   module A = LogicAssigns.Make(M)(L)
 end
 
-module Comp_Region = MakeCompiler(Register(Static)(MemRegion))
+module Comp_Region = MakeCompiler(Register(MemVar.Static)(MemRegion))
 module Comp_MemZeroAlias = MakeCompiler(MemZeroAlias)
 module Comp_Hoare_Raw = MakeCompiler(Model_Hoare_Raw)
 module Comp_Hoare_Ref = MakeCompiler(Model_Hoare_Ref)
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 8bf846d8d084393897f903a8b04b0bbe2f2edf60..337c7854c10053c8d4906c9cd17b45c8613f7563 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -40,6 +40,30 @@ sig
   val iter: ?kf:kernel_function -> init:bool -> (varinfo -> unit) -> unit
 end
 
+module Raw : VarUsage =
+struct
+  let datatype = "Raw"
+  let param _x = MemoryContext.ByValue
+  let iter ?kf ~init f =
+    begin
+      ignore init ;
+      Globals.Vars.iter (fun x _initinfo -> f x) ;
+      match kf with
+      | None -> ()
+      | Some kf -> List.iter f (Kernel_function.get_formals kf) ;
+    end
+end
+
+module Static : VarUsage =
+struct
+  let datatype = "Static"
+  let param x =
+    let open Cil_types in
+    if x.vaddrof || Cil.isArrayType x.vtype || Cil.isPointerType x.vtype
+    then MemoryContext.ByAddr else MemoryContext.ByValue
+  let iter = Raw.iter
+end
+
 module Make(V : VarUsage)(M : Sigs.Model) =
 struct
 
diff --git a/src/plugins/wp/MemVar.mli b/src/plugins/wp/MemVar.mli
index 41de1b22611dff79ff7246913afeb93c37388d2b..b57875390b913c548a6a9854eb1783bac0be447e 100644
--- a/src/plugins/wp/MemVar.mli
+++ b/src/plugins/wp/MemVar.mli
@@ -34,4 +34,12 @@ sig
 
 end
 
+(** VarUsage naive instance.
+    It reports a by-value access for all variables. *)
+module Raw : VarUsage
+
+(** VarUsage that uses only Cil-Static infos. *)
+module Static : VarUsage
+
+(** Create a mixed Hoare Memory Model from VarUsage instance. *)
 module Make(V : VarUsage)(M : Sigs.Model) : Sigs.Model