Wp.Cache
val set_mode : mode -> unit
val get_mode : unit -> mode
val is_active : mode -> bool
val is_updating : mode -> bool
type 'a digest = Why3Provers.t -> 'a -> string
type 'a runner =
timeout:float option ->
steplimit:int option ->
Why3Provers.t ->
'a ->
VCS.result Frama_c_kernel.Task.task
val promote : ?timeout:float -> ?steplimit:int -> VCS.result -> VCS.result
Converts some known results to the given limits. In particular, if the result shall be discarded with respect to the limits, the function returns VCS.no_result
.
val clear_result : digest:'a digest -> Why3Provers.t -> 'a -> unit