diff --git a/.gitignore b/.gitignore
index 6e056235f64c7cd8cd500327d9f0d8ef537e3866..0a653f944d8129668dfeb79de354d6da3f54c9dc 100644
--- a/.gitignore
+++ b/.gitignore
@@ -99,8 +99,8 @@ autom4te.cache
/doc/code/print_api/dynamic_plugins.mli
/doc/code/print_api/_build/
+/doc/code/builtin
/doc/code/studia
-
/doc/code/qed
/doc/code/wp
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 699745967d929230091a915a67daa2544e1a648b..8824f51b8b9c3aaaf4878bce0334ccd62b0e5f47 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -1062,10 +1062,97 @@ end
(** {2 GUI} *)
(* ************************************************************************* *)
-let progress = ref (fun () -> ())
+type daemon = {
+ trigger : unit -> unit ;
+ on_delayed : (int -> unit) option ;
+ debounced : float ; (* in ms *)
+ mutable next_at : float ; (* next trigger time *)
+ mutable last_yield_at : float ; (* last yield time *)
+}
+
+(* ---- Registry ---- *)
+
+let daemons = ref []
+
+let on_progress ?(debounced=0) ?on_delayed trigger =
+ let d = {
+ trigger ;
+ debounced = float debounced /. 1000.0 ;
+ on_delayed ;
+ last_yield_at = 0.0 ;
+ next_at = 0.0 ;
+ } in
+ daemons := List.append !daemons [d] ; d
+
+let off_progress d =
+ daemons := List.filter (fun d0 -> d != d0) !daemons
+
+(* ---- Canceling ---- *)
exception Cancel
+(* ---- Processing ---- *)
+
+let warn_error exn =
+ Kernel.failure
+ "Unexpected Db.daemon exception:@\n%s"
+ (Printexc.to_string exn)
+
+let with_progress ?debounced ?on_delayed trigger job data =
+ let d = on_progress ?debounced ?on_delayed trigger in
+ let result =
+ try job data with e ->
+ off_progress d ;
+ raise e
+ in
+ off_progress d ; result
+
+(* ---- Yielding ---- *)
+
+let canceled = ref false
+let cancel () = canceled := true
+
+let yield () =
+ match !daemons with
+ | [] -> ()
+ | ds ->
+ begin
+ let t = Unix.gettimeofday () in
+ List.iter
+ (fun d ->
+ if t > d.next_at then
+ begin
+ try
+ d.next_at <- t +. d.debounced ;
+ d.trigger () ;
+ with
+ | Cancel -> canceled := true
+ | exn -> warn_error exn ; raise exn
+ end ;
+ match d.on_delayed with
+ | None ->
+ ()
+ | Some _ when d.last_yield_at = 0. ->
+ (* first yield *)
+ d.last_yield_at <- t
+ | Some warn ->
+ let time_since_last_yield = t -. d.last_yield_at in
+ let delay = if d.debounced > 0.0 then d.debounced else 0.1 in
+ if time_since_last_yield > delay then
+ warn (int_of_float (time_since_last_yield *. 1000.0)) ;
+ d.last_yield_at <- t)
+ ds;
+ if !canceled then ( canceled := false ; raise Cancel )
+ end
+
+let flush () =
+ List.iter (fun d -> d.next_at <- 0.0) !daemons ;
+ yield ()
+
+let progress = ref (Kernel.deprecated "!Db.progress()" ~now:"Db.yield()" yield)
+
+(* ************************************************************************* *)
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/plugin_entry_points/db.mli b/src/kernel_services/plugin_entry_points/db.mli
index b37707a8ae7b1d07f2a3d5ee08266868707eb9c0..407b37ea8f33d57ebc277e4c8fdf487f4b7e5a95 100644
--- a/src/kernel_services/plugin_entry_points/db.mli
+++ b/src/kernel_services/plugin_entry_points/db.mli
@@ -1339,6 +1339,61 @@ module Derefs : INOUT with type t = Locations.Zone.t
@plugin development guide *)
val progress: (unit -> unit) ref
+(** Registered daemon on progress. *)
+type daemon
+
+(**
+
+ [on_progress ?debounced ?on_delayed trigger] registers [trigger] as new
+ daemon to be executed on each [yield].
+ @param debounced the least amount of time, in milliseconds, between two
+ successive calls to the daemon (default is 0ms).
+ @param on_delayed the callback invoked as soon as the time since the last
+ [yield] is greater than [debounced] milliseconds (or 100ms at least).
+*)
+val on_progress :
+ ?debounced:int -> ?on_delayed:(int -> unit) -> (unit -> unit) -> daemon
+
+(** Unregister the [daemon]. *)
+val off_progress : daemon -> unit
+
+(** Trigger all daemons immediately. *)
+val flush : unit -> unit
+
+(** Trigger all registered daemons (debounced). *)
+val yield : unit -> unit
+
+(** Interrupt the currently running job.
+ The next call to [Db.yield()] will raise a [Cancel] exception. *)
+val cancel : unit -> unit
+
+(**
+ [with_progress ?debounced ?on_delayed trigger job data] executes the given
+ [job] on [data] while registering [trigger] as temporary (debounced) daemon.
+ The daemon is finally unregistered at the end of the computation.
+ @param debounced the least amount of time, in milliseconds, between two
+ successive calls to the daemon (default is 0ms).
+ @param on_delayed the callback invoked as soon as the time since the last
+ [yield] is greater than [debounced] milliseconds (or 100ms at least).
+ @raise every exception raised during the execution of [job] on [data].
+
+ Illustrative example, where [...] is the debounced time:
+ {[
+ job data : |<-------------------------------------------------->|<daemon removed>
+ yields : x x x x x x x x xxx xxx
+ trigger : |.......... |.......... |.......... |.........
+ delayed : !
+ notes : (1) (2) (3)
+ ]}
+
+ 1. First yield, normal trigger
+ 2. Debounced yields leads to this second trigger
+ 3. Delayed warning invoked since there was no yield for more than debounced period
+*)
+val with_progress :
+ ?debounced:int -> ?on_delayed:(int -> unit) ->
+ (unit -> unit) -> ('a -> 'b) -> 'a -> 'b
+
(** This exception may be raised by {!progress} to interrupt computations. *)
exception Cancel
diff --git a/src/libraries/utils/command.ml b/src/libraries/utils/command.ml
index f11b1065d5e4a0b1eb3d41f9fb4ab6398219c0b4..14bedfcb05cc34a05562b05e2aad364f4b03827e 100644
--- a/src/libraries/utils/command.ml
+++ b/src/libraries/utils/command.ml
@@ -45,7 +45,7 @@ let pp_from_file fmt file =
let cin = open_in file in
try
while true do
- !Db.progress () ;
+ Db.yield () ;
let line = input_line cin in
Format.pp_print_string fmt line ;
Format.pp_print_newline fmt () ;
@@ -248,7 +248,7 @@ let command ?(timeout=0) ?stdout ?stderr cmd args =
| Not_ready terminate ->
begin
try
- !Db.progress () ;
+ Db.yield () ;
if timeout > 0 && Unix.gettimeofday () -. !start > ftimeout then
raise Db.Cancel ;
true
diff --git a/src/libraries/utils/task.ml b/src/libraries/utils/task.ml
index 7750a6c5c9a1e6d78f4d6bc40b3c5bcea52576f3..be822879c38ffab22af0dfdc48b49378e35719fc 100644
--- a/src/libraries/utils/task.ml
+++ b/src/libraries/utils/task.ml
@@ -108,8 +108,8 @@ struct
let rec wait = function
| UNIT a -> a
- | YIELD f -> !Db.progress() ; wait (f Coin)
- | WAIT(ms,f) -> !Db.progress() ; Extlib.usleep ms ; wait (f Coin)
+ | YIELD f -> Db.yield() ; wait (f Coin)
+ | WAIT(ms,f) -> Db.yield() ; Extlib.usleep ms ; wait (f Coin)
let finished = function UNIT a -> Some a | YIELD _ | WAIT _ -> None
@@ -479,7 +479,7 @@ let rec run_server server () =
) server.running ;
Array.iter (schedule server) server.queue ;
try
- !Db.progress () ;
+ Db.yield ();
fire server.activity ;
if server.running <> [] then
begin
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index ea103a92baa5bd002f4c8377783de31e6a8dcf48..87c04563112f04c11290486bec38837ce1a8e2ca 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -353,7 +353,7 @@ struct
~exact access state.deps_table loc deps }
let transfer_call stmt dest f args _loc state =
- !Db.progress ();
+ Db.yield ();
let value_state = To_Use.get_value_state stmt in
let f_deps, called_vinfos =
!Db.Value.expr_to_kernel_function_state
@@ -456,7 +456,7 @@ struct
result
let transfer_instr stmt (i: instr) (state: t) =
- !Db.progress ();
+ Db.yield ();
match i with
| Set (lv, exp, _) ->
let comp_vars = find stmt state.deps_table exp in
@@ -688,7 +688,7 @@ struct
s := !s^" <-"^(Format.asprintf "%a" Kernel_function.pretty kf))
call_stack;
!s);
- !Db.progress ();
+ Db.yield ();
let result =
if !Db.Value.use_spec_instead_of_definition kf
then compute_using_prototype kf
@@ -697,7 +697,7 @@ struct
let result = To_Use.cleanup_and_save kf result in
From_parameters.feedback
"Done for function %a" Kernel_function.pretty kf;
- !Db.progress ();
+ Db.yield ();
CurrentLoc.set call_site_loc;
result
diff --git a/src/plugins/gui/analyses_manager.ml b/src/plugins/gui/analyses_manager.ml
index 787a26083c232db5a65042182e836aba4ff9dcc3..9d3dee429ad0615e9314a62c1629477c460a9fe2 100644
--- a/src/plugins/gui/analyses_manager.ml
+++ b/src/plugins/gui/analyses_manager.ml
@@ -57,7 +57,6 @@ let run_module =
let insert (main_ui: Design.main_window_extension_points) =
let menu_manager = main_ui#menu_manager () in
- let stop = ref (fun () -> assert false) (* delayed *) in
let stop_sensitive = ref false (* can the stop button be clicked? *) in
let default_analyses_items =
menu_manager#add_plugin
@@ -69,31 +68,22 @@ let insert (main_ui: Design.main_window_extension_points) =
(Menu_manager.Unit_callback (fun () -> run_module main_ui));
Menu_manager.toolbar ~sensitive:(fun () -> !stop_sensitive) ~icon:`STOP
~label:"Stop" ~tooltip:"Stop currently running analyses"
- (Menu_manager.Unit_callback (fun () -> !stop ()));
+ (Menu_manager.Unit_callback Db.cancel)
]
in
default_analyses_items.(0)#add_accelerator `CONTROL 'r';
let stop_button = Extlib.the default_analyses_items.(2)#tool_button in
- let old_progress = ref !Db.progress in
- stop :=
- (fun () ->
- Db.progress :=
- (fun () ->
- Db.progress := !old_progress;
- raise Db.Cancel));
Gtk_helper.register_locking_machinery
~lock_last:true
~lock:(fun cancelable ->
if !stop_sensitive then Gui_parameters.warning
"Inconsistent state for stop button. Ignoring.";
- old_progress := !Db.progress;
menu_manager#set_sensitive false;
if cancelable then (stop_button#misc#set_sensitive true;
stop_sensitive := true);
)
~unlock:(fun () ->
- Db.progress := !old_progress;
menu_manager#set_sensitive true;
stop_button#misc#set_sensitive false;
stop_sensitive := false;
diff --git a/src/plugins/gui/design.ml b/src/plugins/gui/design.ml
index 4cf526308c22f254727310396baed427c6e28708..4b926e21ca0edd49abdc694f4df9ef91baee112f 100644
--- a/src/plugins/gui/design.ml
+++ b/src/plugins/gui/design.ml
@@ -1845,7 +1845,7 @@ let make_splash () =
let toplevel play =
Gtk_helper.Configuration.load ();
- Db.progress := Gtk_helper.refresh_gui;
+ ignore (Db.on_progress Gtk_helper.refresh_gui) ;
let in_idle () =
let tid, splash_out, splash_w, reparent_console, force_s= make_splash () in
let error_manager =
diff --git a/src/plugins/impact/compute_impact.ml b/src/plugins/impact/compute_impact.ml
index 9755c2489b728b74a59b81d49b507f9db090d7ea..9bb6b38920a5b16eb7a643c00f48d180d854592a 100644
--- a/src/plugins/impact/compute_impact.ml
+++ b/src/plugins/impact/compute_impact.ml
@@ -577,7 +577,7 @@ let rec intraprocedural wl = match pick wl with
| Some (pnode, { kf; pdg; init; zone }) ->
let node = pnode, zone in
add_to_result wl node kf init;
- !Db.progress ();
+ Db.yield ();
Options.debug ~level:2 "considering new node %a in %a:@ <%a>%t"
PdgTypes.Node.pretty pnode Kernel_function.pretty kf
Pdg_aux.pretty_node node
diff --git a/src/plugins/occurrence/register.ml b/src/plugins/occurrence/register.ml
index 2842ba4673991dfc8a8d96b4ab331c21dcb1dc02..d2aca0a1c8e9084f7c6650279525f9f03993ef20 100644
--- a/src/plugins/occurrence/register.ml
+++ b/src/plugins/occurrence/register.ml
@@ -135,7 +135,7 @@ class occurrence = object (self)
DoChildren
method! vstmt_aux s =
- !Db.progress ();
+ Db.yield ();
super#vstmt_aux s
initializer !Db.Value.compute ()
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 8d0c5ba63a37452d073c75c0ed816cc4c5849a5b..8fbfb29d894c58f3eda661b91f9b88524ae29b80 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -863,7 +863,7 @@ module Computer
(** Compute the new state after 'instr' starting from state before 'state'.
*)
let doInstr stmt instr state =
- !Db.progress ();
+ Db.yield ();
pdg_debug "doInstr sid:%d : %a" stmt.sid Printer.pp_instr instr;
match instr with
| _ when not (Db.Value.is_reachable_stmt stmt) ->
@@ -872,12 +872,12 @@ module Computer
| Local_init (v, AssignInit i, _) ->
process_init current_pdg state stmt (Cil.var v) i
| Local_init (v, ConsInit (f, args, kind), loc) ->
- !Db.progress ();
+ Db.yield ();
Cil.treat_constructor_as_func
(process_call current_pdg state stmt) v f args kind loc
| Set (lv, exp, _) -> process_asgn current_pdg state stmt lv exp
| Call (lvaloption,funcexp,argl,loc) ->
- !Db.progress ();
+ Db.yield ();
process_call current_pdg state stmt lvaloption funcexp argl loc
| Code_annot _
| Skip _ -> process_skip current_pdg state stmt
diff --git a/src/plugins/postdominators/compute.ml b/src/plugins/postdominators/compute.ml
index f766ae37ba196f9f95ca10abdae2be3a06f29bc3..1e65b7b9b838bfde6837c0346aa24fb2eb0013b6 100644
--- a/src/plugins/postdominators/compute.ml
+++ b/src/plugins/postdominators/compute.ml
@@ -118,7 +118,7 @@ struct
let combineSuccessors = DomSet.inter
let doStmt stmt =
- !Db.progress ();
+ Db.yield ();
Postdominators_parameters.debug ~level:2 "doStmt: %d" stmt.sid;
match stmt.skind with
| Return _ -> Dataflow2.Done (DomSet.Value (Stmt.Hptset.singleton stmt))
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
index 9d0e1f4dff6173df2371db624d95f0b72547e0eb..c628ffc4c34e7ec16a7d25382b15ac7660f02130 100644
--- a/src/plugins/server/main.ml
+++ b/src/plugins/server/main.ml
@@ -87,14 +87,13 @@ type 'a exec = {
}
type 'a server = {
- rate : int ;
+ yield : int ;
pretty : Format.formatter -> 'a -> unit ;
equal : 'a -> 'a -> bool ;
fetch : unit -> 'a message option ;
q_in : 'a exec Queue.t ;
q_out : 'a response Stack.t ;
mutable shutdown : bool ;
- mutable coins : int ;
mutable running : 'a exec option ;
}
@@ -132,8 +131,6 @@ let pp_response pp fmt (r : _ response) =
(* --- Request Handling --- *)
(* -------------------------------------------------------------------------- *)
-let no_yield () = ()
-
let execute exec : _ response =
try
let data = exec.handler exec.data in
@@ -147,38 +144,14 @@ let execute exec : _ response =
exec.request (Cmdline.protect exn) ;
`Error(exec.id,Printexc.to_string exn)
-let acceptable_between_yield = 0.25 (* seconds *)
-
-let execute_with_yield yield exec =
- let db = !Db.progress in
- let yield, check =
+let execute_debug server yield exec =
+ let on_delayed =
if Senv.debug_atleast 1 then
- let time = ref (Unix.gettimeofday ()) in
- let check () =
- let time' = Unix.gettimeofday () in
- let diff = time' -. !time in
- if diff > acceptable_between_yield
- then
- Senv.debug
- "Db.progress missing during %s request (spent %fs between calls)"
- exec.request
- diff
- in
- (fun () ->
- check ();
- yield ();
- time := Unix.gettimeofday ()),
- check
- else
- yield, ignore
- in
- Db.progress := if exec.yield then yield else no_yield;
- Extlib.try_finally ~finally:(fun () -> Db.progress := db; check ()) execute exec
-
-let execute_debug pp yield exec =
- if Senv.debug_atleast 1 then
- Senv.debug "Trigger %s:%a" exec.request pp exec.id ;
- execute_with_yield yield exec
+ (Senv.debug "Trigger %s:%a" exec.request server.pretty exec.id ;
+ Some (fun delay -> Senv.debug
+ "No yield since %dms during %s" delay exec.request))
+ else None
+ in Db.with_progress ~debounced:server.yield ?on_delayed yield execute exec
let reply_debug server resp =
if Senv.debug_atleast 1 then
@@ -253,11 +226,7 @@ let communicate server =
let do_yield server () =
begin
option raise_if_killed server.running ;
- let n = server.coins in
- if n < server.rate then
- server.coins <- succ n
- else
- ( server.coins <- 0 ; ignore ( communicate server ) ) ;
+ ignore ( communicate server );
end
(* -------------------------------------------------------------------------- *)
@@ -276,7 +245,7 @@ let process server =
| Some exec ->
server.running <- Some exec ;
try
- reply_debug server (execute_debug server.pretty (do_yield server) exec) ;
+ reply_debug server (execute_debug server (do_yield server) exec) ;
server.running <- None ;
true
with exn ->
@@ -290,7 +259,6 @@ let process server =
let in_range ~min:a ~max:b v = min (max a v) b
let kill () = raise Killed
-let yield () = !Db.progress ()
let demons = ref []
let on callback = demons := !demons @ [ callback ]
@@ -299,11 +267,11 @@ let signal activity =
let run ~pretty ?(equal=(=)) ~fetch () =
begin
- let rate = in_range ~min:1 ~max:200 (Senv.Rate.get ()) in
+ let yield = in_range ~min:1 ~max:200 (Senv.Yield.get ()) in
let idle_ms = in_range ~min:1 ~max:2000 (Senv.Idle.get ()) in
- let idle_s = float_of_int idle_ms /. 1000.0 in
+ let idle = float_of_int idle_ms /. 1000.0 in
let server = {
- fetch ; coins = 0 ; rate ; equal ; pretty ;
+ fetch ; yield ; equal ; pretty ;
q_in = Queue.create () ;
q_out = Stack.create () ;
running = None ;
@@ -318,7 +286,7 @@ let run ~pretty ?(equal=(=)) ~fetch () =
begin try
while not server.shutdown do
let activity = process server in
- if not activity then Unix.sleepf idle_s ;
+ if not activity then Unix.sleepf idle ;
done ;
with Sys.Break -> () (* Ctr+C, just leave the loop normally *)
end;
diff --git a/src/plugins/server/main.mli b/src/plugins/server/main.mli
index 721291d96e9b93c4d65676fb83b216fafba39bd7..75d51a0d17af477241683a5ccdc2c5915210dfe3 100644
--- a/src/plugins/server/main.mli
+++ b/src/plugins/server/main.mli
@@ -81,10 +81,6 @@ val run :
fetch:(unit -> 'a message option) ->
unit -> unit
-(** Yield the server during the currently running request.
- Actually, calls [!Db.progress()]. *)
-val yield : unit -> unit
-
(** Kills the currently running request. Actually raises an exception. *)
val kill : unit -> 'a
diff --git a/src/plugins/server/server_parameters.ml b/src/plugins/server/server_parameters.ml
index 76a572cdf0cbd164afcf0c948b5fec0f9f40e9a6..57dbdd133f9f088015fe82df6ea19932565b883f 100644
--- a/src/plugins/server/server_parameters.ml
+++ b/src/plugins/server/server_parameters.ml
@@ -37,16 +37,16 @@ module Idle = P.Int
(struct
let option_name = "-server-idle"
let arg_name = "ms"
- let default = 10
+ let default = 20
let help = "Waiting time (in milliseconds) when idle"
end)
-module Rate = P.Int
+module Yield = P.Int
(struct
- let option_name = "-server-rate"
- let arg_name = "n"
- let default = 100
- let help = "Number of analysis steps between server communications"
+ let option_name = "-server-yield"
+ let arg_name = "ms"
+ let default = 20
+ let help = "Yielding time (in milliseconds) during computations"
end)
module Doc = P.String
diff --git a/src/plugins/server/server_parameters.mli b/src/plugins/server/server_parameters.mli
index 5dc5ad153438ddc07353cb1b93cc59f22d4e91de..9bbd8a148fde84d797559b9675f44098c42e59c7 100644
--- a/src/plugins/server/server_parameters.mli
+++ b/src/plugins/server/server_parameters.mli
@@ -25,7 +25,7 @@
include Plugin.General_services
module Idle : Parameter_sig.Int (** Idle waiting time (in ms) *)
-module Rate : Parameter_sig.Int (** Number of fetch per yield *)
+module Yield : Parameter_sig.Int (** Yield time (in ms) *)
module Doc : Parameter_sig.String (** Generate documentation *)
module Log : Parameter_sig.Bool (** Monitor logs *)
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 96bced78522acc52b351e9dc1502e87d32ef3a95..cc122f92ae9f36e93fb5d47b4a370cabe8620dc2 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -420,7 +420,7 @@ module Make_Dataflow
let {edge_transition=transition; edge_kinstr=kinstr} = e in
let tank,edge_info = get_edge_data e in
let flow = Partition.drain tank in
- !Db.progress ();
+ Db.yield ();
check_signals ();
current_ki := kinstr;
Cil.CurrentLoc.set e.edge_loc;
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index f203b8b5cd7187ce016ee7d3f3319ce68ac0e703..021ef13b877c4b9336a8c32d1681fbc58ae97f0e 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -1095,7 +1095,7 @@ end
let rec fixpoint limit solvers sigma s0 =
if limit > 0 then compute limit solvers sigma s0 else s0
and compute limit solvers sigma s0 =
- !Db.progress ();
+ Db.yield ();
let s1 =
if Wp_parameters.Ground.get () then ground s0
else s0 in
@@ -1158,7 +1158,7 @@ let tc = ref 0
let rec test_cases (s : hsp) = function
| [] -> s
| (p,_) :: tail ->
- !Db.progress () ;
+ Db.yield () ;
match test_case p s , test_case (p_not p) s with
| None , None -> incr tc ; [],F.p_true
| Some w , None -> incr tc ; test_cases w tail
diff --git a/src/plugins/wp/calculus.ml b/src/plugins/wp/calculus.ml
index 8f5b282c90ddfb87b51d6bb32c75531ee6d662d3..e6d6bf8cdd91ee0b4a81aa2300c864f427515d8c 100644
--- a/src/plugins/wp/calculus.ml
+++ b/src/plugins/wp/calculus.ml
@@ -500,7 +500,7 @@ module Cfg (W : Mcfg.S) = struct
(** @return the WP stored for edge [e]. Compute it if it is not already
* there and store it. Also handle the Acut annotations. *)
let rec get_wp_edge ((_kf, cfg, strategy, res, wenv) as env) e =
- !Db.progress ();
+ Db.yield ();
let v = Cil2cfg.edge_dst e in
debug "[get_wp_edge] get wp before %a@." Cil2cfg.pp_node v;
try
diff --git a/src/plugins/wp/cil2cfg.ml b/src/plugins/wp/cil2cfg.ml
index d009c01f0409bc5bae959915b12f2789d156449c..01e38dc3a82cbd01fefb8719b5a38bc70bc587f7 100644
--- a/src/plugins/wp/cil2cfg.ml
+++ b/src/plugins/wp/cil2cfg.ml
@@ -853,7 +853,7 @@ and cfg_switch env switch_stmt switch_exp blk case_stmts next =
n_switch
and cfg_stmt env s next =
- !Db.progress ();
+ Db.yield ();
match s.skind with
| Instr (Call (_, f, _, _)) ->
setup_preconditions_proxies f;
@@ -1220,11 +1220,11 @@ let cfg_from_definition kf f =
kf_name (CFG.nb_edges graph) (CFG.nb_vertex graph);
debug
"start removing unreachable in %s@." kf_name;
- !Db.progress ();
+ Db.yield ();
let cfg = clean_graph cfg in
debug "for function '%s': %d vertex - %d edges@."
kf_name (CFG.nb_edges graph) (CFG.nb_vertex graph);
- !Db.progress ();
+ Db.yield ();
debug
"start loop analysis for %s@." kf_name;
let cfg = mark_loops cfg in
@@ -1249,7 +1249,7 @@ let create kf =
with Kernel_function.No_Definition ->
cfg_from_proto kf
in debug "done for %s@." kf_name;
- !Db.progress ();
+ Db.yield ();
cfg
module KfCfg =