diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 0a40a62ac09b77f558e5a76caff32d7dc783b44b..fe83f4ddfba4ae02fa79e98f69294f6e6f3cb658 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -386,6 +386,36 @@ class behavior
 
   end
 
+(* -------------------------------------------------------------------------- *)
+(* --- Model Info for Variables                                           --- *)
+(* -------------------------------------------------------------------------- *)
+
+let model_varinfo :
+  GMenu.menu GMenu.factory ->
+  Design.main_window_extension_points ->
+  button:int -> Pretty_source.localizable -> unit =
+  fun _menu main ~button item ->
+    let open Pretty_source in
+    let open Cil_types in
+    match item with
+    | PLval(Some kf, _ , (Var x,NoOffset))
+    | PTermLval(Some kf, _, _, (TVar {lv_origin=Some x},TNoOffset))
+      when button=1 ->
+        let init = WpStrategy.is_main_init kf in
+        let acc = RefUsage.get ~kf ~init x in
+        let model = match acc with
+          | RefUsage.NoAccess -> "any"
+          | RefUsage.ByValue -> "'var'"
+          | RefUsage.ByRef -> "'ref'"
+          | RefUsage.ByArray when x.vformal && Cil.isPointerType x.vtype
+            -> "'caveat'"
+          | _ -> "'typed'"
+        in
+        main#pretty_information
+          "Is is accessed as %t and fits in %s wp-model@."
+          (RefUsage.print x acc) model ;
+    | _ -> ()
+
 (* -------------------------------------------------------------------------- *)
 (* --- Make Panel and Extend Frama-C GUI                                  --- *)
 (* -------------------------------------------------------------------------- *)
@@ -491,6 +521,7 @@ let make (main : main_window_extension_points) =
     ignore (main#lower_notebook#append_page ~tab_label panel#coerce) ;
     main#register_source_highlighter source#highlight ;
     main#register_source_selector popup#register ;
+    main#register_source_selector model_varinfo ;
 
     GuiPanel.register ~main
       ~configure_provers:dp_chooser#run ;
diff --git a/src/plugins/wp/RefUsage.ml b/src/plugins/wp/RefUsage.ml
index 38647c7e307cf9b980f174c82d078a23d1ebe8d6..53160d9ae3070bd72330806bc457fbf4084ab11e 100644
--- a/src/plugins/wp/RefUsage.ml
+++ b/src/plugins/wp/RefUsage.ml
@@ -824,6 +824,8 @@ let get ?kf ?(init=false) vi =
 
 let compute () = ignore (usage ())
 
+let print x m fmt = Access.pretty x fmt m
+
 let dump () =
   Log.print_on_output
     begin fun fmt ->
diff --git a/src/plugins/wp/RefUsage.mli b/src/plugins/wp/RefUsage.mli
index 7a50bebcd53f2583d69fbabd16f295037295320e..d68b05f7d487d4e5ac1ae00f4385160aa5659d10 100644
--- a/src/plugins/wp/RefUsage.mli
+++ b/src/plugins/wp/RefUsage.mli
@@ -37,5 +37,6 @@ val get : ?kf:kernel_function -> ?init:bool -> varinfo -> access
 
 val iter: ?kf:kernel_function -> ?init:bool -> (varinfo -> access -> unit) -> unit
 
+val print : varinfo -> access -> Format.formatter -> unit
 val dump : unit -> unit
 val compute : unit -> unit