From 2712368c3b76fcfb99d2558f84d5cb1716ea43f7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 17 Jan 2023 12:07:58 +0100
Subject: [PATCH] [kernel] New hook called at each update of a property status.
---
src/kernel_services/ast_data/property_status.ml | 8 ++++++++
src/kernel_services/ast_data/property_status.mli | 5 +++++
2 files changed, 13 insertions(+)
diff --git a/src/kernel_services/ast_data/property_status.ml b/src/kernel_services/ast_data/property_status.ml
index 26eba1a5c8a..44387df98db 100644
--- a/src/kernel_services/ast_data/property_status.ml
+++ b/src/kernel_services/ast_data/property_status.ml
@@ -392,6 +392,13 @@ module Register_hook = Hook.Build (struct type t = Property.t end)
let register_property_add_hook = Register_hook.extend
+module Status_hook = Hook.Build
+ (struct type t = emitter_with_properties * Property.t * emitted_status end)
+
+let register_status_update_hook f =
+ Status_hook.extend
+ (fun (emitter, property, status) -> f emitter property status)
+
let rec register ppt =
Kernel.debug ~dkey:Kernel.dkey_prop_status_reg
"REGISTERING %a in %a"
@@ -486,6 +493,7 @@ and unsafe_emit_and_get e ~hyps ~auto ppt ?(distinct=false) s =
add { emitter with properties = [ reach_ppt ] } s
| _ :: _ -> Kernel.fatal "Emitter %a proves invalidity of %a under \
hypotheses: unsound!" Emitter.pretty e Property.pretty ppt));
+ Status_hook.apply (emitter, ppt, s);
s
in
(try
diff --git a/src/kernel_services/ast_data/property_status.mli b/src/kernel_services/ast_data/property_status.mli
index bbe2f162668..a16f5bcbfb5 100644
--- a/src/kernel_services/ast_data/property_status.mli
+++ b/src/kernel_services/ast_data/property_status.mli
@@ -138,6 +138,11 @@ val fold_on_statuses:
Property.t ->
'a -> 'a
+val register_status_update_hook:
+ (emitter_with_properties -> Property.t -> emitted_status -> unit) -> unit
+(** Registers an hook to be called each time a property status is emitted.
+ @since Frama-C+dev *)
+
(* ************************************************************************ *)
(** {2 Consolidated status} *)
(* ************************************************************************ *)
--
GitLab