Commit 6b4ed04e authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'fix/server/property-status-update' into 'master'

[Ivette] Fixes synchronization of properties status

Closes #1203

See merge request frama-c/frama-c!4054
parents e713f239 1fbb7ff2
......@@ -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
......
......@@ -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} *)
(* ************************************************************************ *)
......@@ -258,7 +263,7 @@ val register: Property.t -> unit
(** Register the given property. It must not be already registered. *)
val register_property_add_hook: (Property.t -> unit) -> unit
(** add an hook that will be called for any newly registered property
(** Add an hook that will be called for any newly registered property
@since Neon-20140301 *)
val remove: Property.t -> unit
......@@ -266,7 +271,7 @@ val remove: Property.t -> unit
corresponding annotation. *)
val register_property_remove_hook: (Property.t -> unit) -> unit
(** Add and hook that will be called each time a property is removed.
(** Add an hook that will be called each time a property is removed.
@since Neon-20140301 *)
val merge: old:Property.t list -> Property.t list -> unit
......
......@@ -322,9 +322,13 @@ let is_relevant ip =
|| 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 add_update_hook f =
Property_status.register_property_add_hook
(fun ip -> if is_relevant ip then f ip)
(fun ip -> if is_relevant ip then f ip);
Property_status.register_status_update_hook
(fun _emitter ip _status -> 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)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment