From 9160209fb734d7341cb7f7514759a9f7b0cf1465 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 21 Apr 2023 17:17:10 +0200
Subject: [PATCH] [kernel] annotations update hook
---
src/kernel_services/ast_data/annotations.ml | 13 +++++++++++++
src/kernel_services/ast_data/annotations.mli | 4 ++++
2 files changed, 17 insertions(+)
diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml
index b30a7a86800..e2b814dc187 100644
--- a/src/kernel_services/ast_data/annotations.ml
+++ b/src/kernel_services/ast_data/annotations.ml
@@ -155,6 +155,19 @@ let () =
let kf = find_englobing_kf stmt in
List.iter (fun a -> clear_linked_to_annot kf stmt e a) !l)
+let add_hook_on_change f =
+ begin
+ let notify _ _ _ = f () in
+ Globals.add_hook_on_update notify ;
+ Globals.add_hook_on_remove notify ;
+ Model_fields.add_hook_on_update notify ;
+ Model_fields.add_hook_on_remove notify ;
+ Funspecs.add_hook_on_update notify ;
+ Funspecs.add_hook_on_remove notify ;
+ Code_annots.add_hook_on_update notify ;
+ Code_annots.add_hook_on_remove notify ;
+ end
+
(**************************************************************************)
(** {2 Getting annotations} *)
(**************************************************************************)
diff --git a/src/kernel_services/ast_data/annotations.mli b/src/kernel_services/ast_data/annotations.mli
index 3d84adb429d..6f1ae71fa54 100644
--- a/src/kernel_services/ast_data/annotations.mli
+++ b/src/kernel_services/ast_data/annotations.mli
@@ -30,6 +30,10 @@ open Cil_types
(** {2 Getting annotations} *)
(**************************************************************************)
+val add_hook_on_change: (unit -> unit) -> unit
+(** Emitted whenever anhy of the annotation tables are modified.
+ @since Frama-C+dev *)
+
(**************************************************************************)
(** {3 Code annotations} *)
(**************************************************************************)
--
GitLab