From 75ccdcff27a8be1e94164ea05b1465adaf04ff69 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 27 May 2020 17:03:12 +0200
Subject: [PATCH] [server] Synchronized property array: do not export all
properties.
---
src/plugins/server/kernel_properties.ml | 21 ++++++++++++++++++---
1 file changed, 18 insertions(+), 3 deletions(-)
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 72812b886a7..968e8fef88d 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -245,15 +245,30 @@ let () = States.column ~model ~name:"source"
~data:(module LogSource)
~get:(fun ip -> Property.location ip |> fst) ()
+let is_relevant ip =
+ match Property.get_kf ip with
+ | None -> true
+ | Some kf ->
+ not (Ast_info.is_frama_c_builtin (Kernel_function.get_name kf)
+ || Cil.is_unused_builtin (Kernel_function.get_vi kf))
+
+let iter f = Property_status.iter (fun ip -> if is_relevant ip then f ip)
+let add_update_hook f =
+ Property_status.register_property_add_hook
+ (fun ip -> if is_relevant ip then f ip)
+let add_remove_hook f =
+ Property_status.register_property_remove_hook
+ (fun ip -> if is_relevant ip then f ip)
+
let array =
States.register_array
~page
~name:"kernel.properties"
~descr:(Md.plain "Registered Properties")
~key:(fun ip -> Kernel_ast.Marker.create (PIP ip))
- ~iter:(Property_status.iter)
- ~add_update_hook:Property_status.register_property_add_hook
- ~add_remove_hook:Property_status.register_property_remove_hook
+ ~iter
+ ~add_update_hook
+ ~add_remove_hook
model
let reload () = States.reload array
--
GitLab