diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index d52363f4281bd136fe28d7872fbaf083cd1f9b7c..7b35a43e95f9ed12433f8dd31990b8cf7377e207 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1210,6 +1210,8 @@ src/plugins/studia/reads.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/reads.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/studia_gui.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/studia_gui.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/studia/studia_request.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/studia/studia_request.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/Studia.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/writes.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/writes.mli: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/studia/Makefile.in b/src/plugins/studia/Makefile.in
index 76fa49dac96432f94679700c99e724905b665c85..c49e1893f2ea65bb13148d6189f58c7b667a2de0 100644
--- a/src/plugins/studia/Makefile.in
+++ b/src/plugins/studia/Makefile.in
@@ -36,7 +36,7 @@ endif
PLUGIN_DIR ?=.
PLUGIN_ENABLE:=@ENABLE_STUDIA@
PLUGIN_NAME:=Studia
-PLUGIN_CMO:= options writes reads
+PLUGIN_CMO:= options writes reads studia_request
PLUGIN_GUI_CMO:= studia_gui
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
diff --git a/src/plugins/studia/studia_request.ml b/src/plugins/studia/studia_request.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0297777d9b0147d901414f4702bc43368b01fef8
--- /dev/null
+++ b/src/plugins/studia/studia_request.ml
@@ -0,0 +1,98 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Server
+open Cil_types
+
+let package =
+ Package.package ~plugin:"studia" ~name:"studia" ~title:"Studia"
+ ~readme:"studia.md" ()
+
+type effects =
+ { direct: stmt list;
+ indirect: stmt list; }
+
+module Effects = struct
+ open Server.Data
+
+ type record
+ let record: record Record.signature = Record.signature ()
+
+ module Location = Data.Jpair (Kernel_ast.Kf) (Kernel_ast.Marker)
+
+ let direct = Record.field record ~name:"direct"
+ ~descr:(Markdown.plain "List of statements with direct effect.")
+ (module Data.Jlist (Location))
+ let indirect = Record.field record ~name:"indirect"
+ ~descr:(Markdown.plain "List of statements with indirect effect.")
+ (module Data.Jlist (Location))
+
+ let data = Record.publish record ~package ~name:"effects"
+ ~descr:(Markdown.plain "Statements that read or write a location.")
+
+ module R : Record.S with type r = record = (val data)
+ type t = effects
+ let jtype = R.jtype
+
+ let to_json effects =
+ let output_stmt stmt =
+ let kf = Kernel_function.find_englobing_kf stmt in
+ kf, Printer_tag.PStmtStart (kf, stmt)
+ in
+ R.default |>
+ R.set direct (List.map output_stmt effects.direct) |>
+ R.set indirect (List.map output_stmt effects.indirect) |>
+ R.to_json
+end
+
+
+type kind = Reads | Writes
+
+let compute kind zone =
+ let stmts = match kind with
+ | Reads -> Reads.compute zone
+ | Writes -> Writes.compute zone
+ in
+ let add_if b stmt acc = if b then stmt :: acc else acc in
+ let add acc (stmt, e) =
+ let direct = add_if e.Writes.direct stmt acc.direct in
+ let indirect = add_if e.Writes.indirect stmt acc.indirect in
+ { direct; indirect }
+ in
+ let empty = { direct = []; indirect = []; } in
+ List.fold_left add empty stmts
+
+let lval_location kinstr lval = !Db.Value.lval_to_zone kinstr lval
+
+let () = Request.register ~package
+ ~kind:`GET ~name:"getReadsLval"
+ ~descr:(Markdown.plain "Get the list of statements that read a lval.")
+ ~input:(module Kernel_ast.Lval)
+ ~output:(module Effects)
+ (fun (kinstr, lval) -> compute Reads (lval_location kinstr lval))
+
+let () = Request.register ~package
+ ~kind:`GET ~name:"getWritesLval"
+ ~descr:(Markdown.plain "Get the list of statements that write a lval.")
+ ~input:(module Kernel_ast.Lval)
+ ~output:(module Effects)
+ (fun (kinstr, lval) -> compute Writes (lval_location kinstr lval))
diff --git a/src/plugins/studia/studia_request.mli b/src/plugins/studia/studia_request.mli
new file mode 100644
index 0000000000000000000000000000000000000000..182bc40a8e1af00f6d1329952d449d0f2e6808e1
--- /dev/null
+++ b/src/plugins/studia/studia_request.mli
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)