From 36b0bf42be3f6d4c9a986c71b8ce304d6b9567c6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 9 Mar 2023 09:52:35 +0100
Subject: [PATCH] [server] clever fix for property status updates
---
src/plugins/server/kernel_properties.ml | 33 ++++++++++++++-----------
1 file changed, 19 insertions(+), 14 deletions(-)
diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml
index 46bf49f941a..e5c7b393fff 100644
--- a/src/plugins/server/kernel_properties.ml
+++ b/src/plugins/server/kernel_properties.ml
@@ -321,7 +321,22 @@ let is_relevant ip =
not (Ast_info.is_frama_c_builtin (Kernel_function.get_name kf)
|| Cil_builtins.is_unused_builtin (Kernel_function.get_vi kf))
-let iter f = Property_status.iter (fun ip -> if is_relevant ip then f ip)
+let iter f =
+ Property_status.iter (fun ip -> if is_relevant ip then f ip)
+
+(* Must reload the entire table when status changed: property dependencies
+ are not taken into account when status are updated. *)
+let add_reload_hook (f : unit -> unit) : unit =
+ Property_status.register_status_update_hook
+ (fun _emitter _ip _status -> f())
+
+let add_update_hook (f : Property.t -> unit) : unit =
+ Property_status.register_property_add_hook
+ (fun ip -> if is_relevant ip then f ip)
+
+let add_remove_hook (f : Property.t -> unit) : unit =
+ Property_status.register_property_remove_hook
+ (fun ip -> if is_relevant ip then f ip)
let array =
States.register_array
@@ -331,21 +346,11 @@ let array =
~key:(fun ip -> Kernel_ast.Marker.create (PIP ip))
~keyType:Kernel_ast.Marker.jproperty
~iter
+ ~add_reload_hook
+ ~add_remove_hook
+ ~add_update_hook
model
let reload () = States.reload array
-(* Reloads the whole array when a property is added, removed or when its status
- changes. As a property can be a logical consequence of other properties, a
- property change can impact the logical status of any other property: a full
- reload is needed. *)
-let () =
- Property_status.register_property_add_hook
- (fun _ip -> reload ());
- Property_status.register_status_update_hook
- (fun _emitter _ip _status -> reload ());
- Property_status.register_property_remove_hook
- (fun _ip -> reload ())
-
-
(* -------------------------------------------------------------------------- *)
--
GitLab