From a12dd4df676181f23dce2d97b2cab20d183f16a4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 13 Feb 2020 18:18:13 +0100
Subject: [PATCH] [server] (projectified) states & values
---
src/plugins/server/Makefile.in | 3 +-
src/plugins/server/states.ml | 58 ++++++++++++++++++++++++++++++++++
src/plugins/server/states.mli | 42 ++++++++++++++++++++++++
3 files changed, 102 insertions(+), 1 deletion(-)
create mode 100644 src/plugins/server/states.ml
create mode 100644 src/plugins/server/states.mli
diff --git a/src/plugins/server/Makefile.in b/src/plugins/server/Makefile.in
index 48b3e23e469..8ea6491e503 100644
--- a/src/plugins/server/Makefile.in
+++ b/src/plugins/server/Makefile.in
@@ -39,7 +39,8 @@ PLUGIN_NAME:=Server
PLUGIN_CMO:= \
server_parameters \
jbuffer \
- doc syntax data main request \
+ doc syntax data \
+ main request states \
server_batch \
kernel_main \
kernel_project \
diff --git a/src/plugins/server/states.ml b/src/plugins/server/states.ml
new file mode 100644
index 00000000000..f3af381df65
--- /dev/null
+++ b/src/plugins/server/states.ml
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Values & States --- *)
+(* -------------------------------------------------------------------------- *)
+
+let register_value (type a) ~page ~name ~descr ?(details=[])
+ ~(output : a Request.output) ~get =
+ let open Markdown in
+ let title = Printf.sprintf "`VALUE` %s" name in
+ let index = [ Printf.sprintf "%s (`VALUE`)" name ] in
+ let description = [ Block [Text descr] ; Block details] in
+ let h = Doc.publish ~page ~name ~title ~index description [] in
+ let signal = Request.signal ~page ~name:(name ^ ".sig")
+ ~descr:(plain "Signal for value " @ href h) () in
+ Request.register ~page ~kind:`GET ~name:(name ^ ".get")
+ ~descr:(plain "Getter for value " @ href h)
+ ~input:(module Data.Junit) ~output get ;
+ signal
+
+let register_state (type a) ~page ~name ~descr ?(details=[])
+ ~(data : a Data.data) ~get ~set =
+ let open Markdown in
+ let title = Printf.sprintf "`STATE` %s" name in
+ let index = [ Printf.sprintf "%s (`STATE`)" name ] in
+ let description = [ Block [Text descr] ; Block details] in
+ let h = Doc.publish ~page ~name ~title ~index description [] in
+ let signal = Request.signal ~page ~name:(name ^ ".sig")
+ ~descr:(plain "Signal for state " @ href h) () in
+ Request.register ~page ~kind:`GET ~name:(name ^ ".get")
+ ~descr:(plain "Getter for state " @ href h)
+ ~input:(module Data.Junit) ~output:(module (val data)) get ;
+ Request.register ~page ~kind:`SET ~name:(name ^ ".set")
+ ~descr:(plain "Setter for state " @ href h)
+ ~input:(module (val data)) ~output:(module Data.Junit) set ;
+ signal
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/states.mli b/src/plugins/server/states.mli
new file mode 100644
index 00000000000..8bd97b3a34b
--- /dev/null
+++ b/src/plugins/server/states.mli
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val register_value :
+ page:Doc.page ->
+ name:string ->
+ descr:Markdown.text ->
+ ?details:Markdown.block ->
+ output:'a Request.output ->
+ get:(unit -> 'a) ->
+ Request.signal
+
+val register_state :
+ page:Doc.page ->
+ name:string ->
+ descr:Markdown.text ->
+ ?details:Markdown.block ->
+ data:'a Data.data ->
+ get:(unit -> 'a) ->
+ set:('a -> unit) ->
+ Request.signal
+
+(* -------------------------------------------------------------------------- *)
--
GitLab