diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 6dd76c134789afb91c5d3db8ef6eb3213da42721..7f51b3cbee164d0476fbec2cbdf6fc936a447b70 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -254,6 +254,25 @@ module Printer = Printer_tag.Make(Marker)
 (* --- Ast Data                                                           --- *)
 (* -------------------------------------------------------------------------- *)
 
+module Lval =
+struct
+  type t = kinstr * lval
+  let jtype = Marker.jlval
+  let to_json (kinstr, lval) =
+    let kf = match kinstr with
+      | Kglobal -> None
+      | Kstmt stmt -> Some (Kernel_function.find_englobing_kf stmt)
+    in
+    Marker.to_json (PLval (kf, kinstr, lval))
+  let of_json js =
+    let open Printer_tag in
+    match Marker.of_json js with
+    | PLval (_, kinstr, lval) -> kinstr, lval
+    | PVDecl (_, kinstr, vi) -> kinstr, Cil.var vi
+    | PGlobal (GVar (vi, _, _) | GVarDecl (vi, _)) -> Kglobal, Cil.var vi
+    | _ -> Data.failure "not a lval marker"
+end
+
 module Stmt =
 struct
   type t = stmt
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index 6832e10f4ed79ccfd685b8bd8f966de80c09bd63..f9e56c08f27a90fa306f789c5453704a690176c5 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -30,6 +30,7 @@ open Cil_types
 module Kf : Data.S with type t = kernel_function
 module Ki : Data.S with type t = kinstr
 module Stmt : Data.S with type t = stmt
+module Lval : Data.S with type t = kinstr * lval
 
 module Marker :
 sig