[server] properties sync-array

headers/header_spec.txt

@@ -1097,6 +1097,8 @@ src/plugins/server/kernel_main.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/server/kernel_main.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/server/kernel_project.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/server/kernel_project.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/kernel_properties.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/kernel_properties.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/server/main.ml: CEA_LGPL_OR_PROPRIETARY
 src/plugins/server/main.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/server/request.ml: CEA_LGPL_OR_PROPRIETARY

src/plugins/server/Makefile.in

@@ -44,7 +44,9 @@ PLUGIN_CMO:= \
 	server_batch \
 	kernel_main \
 	kernel_project \
-	kernel_ast
+	kernel_ast \
+	kernel_properties
+
 PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
 PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
 PLUGIN_TESTS_DIRS := batch

src/plugins/server/kernel_properties.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+module Sy = Syntax
+module Md = Markdown
+module Js = Yojson.Basic.Util
+
+open Data
+open Kernel_main
+open Kernel_ast
+
+(* -------------------------------------------------------------------------- *)
+(* --- Properties                                                         --- *)
+(* -------------------------------------------------------------------------- *)
+
+let page = Doc.page `Kernel ~title:"Property Services" ~filename:"properties.md"
+
+let model = States.model ()
+
+let () = States.column ~model ~name:"descr"
+    ~descr:(Md.plain "Description")
+    ~data:(module Jstring)
+    ~get:(fun ip -> Format.asprintf "%a" Property.pretty ip) ()
+
+let () = States.column ~model ~name:"status"
+    ~descr:(Md.plain "Status")
+    ~data:(module Jstring)
+    ~get:(fun ip ->
+        let st = Property_status.Feedback.get ip
+        in Format.asprintf "%a" Property_status.Feedback.pretty st) ()
+
+let () = States.column ~model ~name:"function"
+    ~descr:(Md.plain "Function")
+    ~data:(module Kf.Joption) ~get:Property.get_kf ()
+
+let () = States.column ~model ~name:"kinstr"
+    ~descr:(Md.plain "Instruction")
+    ~data:(module Ki) ~get:Property.get_kinstr ()
+
+let () = States.column ~model ~name:"source"
+    ~descr:(Md.plain "Position")
+    ~data:(module LogSource)
+    ~get:(fun ip -> Property.location ip |> fst) ()
+
+let array =
+  States.register_array
+    ~page
+    ~name:"kernel.properties"
+    ~descr:(Md.plain "Registered Properties")
+    ~key:(Property.Names.get_prop_name_id)
+    ~iter:(Property_status.iter)
+    ~add_update_hook:Property_status.register_property_add_hook
+    ~add_remove_hook:Property_status.register_property_remove_hook
+    model
+
+(* -------------------------------------------------------------------------- *)

src/plugins/server/states.ml

@@ -93,14 +93,15 @@ type 'a model = 'a column list ref
 
 let model () = ref []
 
-let column (type a) (m : a model) ~name ~descr (output : a Request.output) =
-  let module D = (val output) in
+let column (type a b) ~(model : a model) ~name ~descr
+    ~(data: b Request.output) ~(get : a -> b) () =
+  let module D = (val data) in
   if name = "id" || name = "_index" then
     raise (Invalid_argument "Server.States.column: invalid name") ;
-  if List.exists (fun (fd,_) -> fd.Syntax.name = name) !m then
+  if List.exists (fun (fd,_) -> fd.Syntax.name = name) !model then
     raise (Invalid_argument "Server.States.column: duplicate name") ;
   let fd = Syntax.{ name ; syntax = D.syntax ; descr } in
-  m := (fd , D.to_json) :: !m
+  model := (fd , fun a -> D.to_json (get a)) :: !model
 
 module Kmap = Map.Make(String)
 

src/plugins/server/states.mli

@@ -77,8 +77,12 @@ val model : unit -> 'a model
     Columns with name `"id"` and `"_index"` are
     reserved for internal use. *)
 val column :
-  'a model -> name:string -> descr:Markdown.text ->
-  'a Request.output -> unit
+  model:'a model ->
+  name:string ->
+  descr:Markdown.text ->
+  data:('b Request.output) ->
+  get:('a -> 'b) ->
+  unit -> unit
 
 type 'a array (** Synchronized array state *)