diff --git a/src/kernel_services/ast_data/annotations.ml b/src/kernel_services/ast_data/annotations.ml index b30a7a868009fcd841748aec094e53cdf69104c1..e2b814dc187d00c7654e32834684b6946f37aada 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 3d84adb429de8fd69bd5644009a5b8a062b515df..6f1ae71fa54224378c987a73c44a8628699c90b8 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} *) (**************************************************************************)