From 3eb0182c45a2fed391d13ef94fa0fcf79ac10a7f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 26 Nov 2020 15:19:49 +0100
Subject: [PATCH] [server] Kernel AST: adds and exports module Lval.

---
 src/plugins/server/kernel_ast.ml  | 19 +++++++++++++++++++
 src/plugins/server/kernel_ast.mli |  1 +
 2 files changed, 20 insertions(+)

diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 6dd76c13478..7f51b3cbee1 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 6832e10f4ed..f9e56c08f27 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
-- 
GitLab