Module Wp.CacheSource

Sourcetype mode =
  1. | NoCache
  2. | Update
  3. | Replay
  4. | Rebuild
  5. | Offline
  6. | Cleanup
Sourceval get_dir : unit -> string
Sourceval set_mode : mode -> unit
Sourceval get_mode : unit -> mode
Sourceval get_hits : unit -> int
Sourceval get_miss : unit -> int
Sourceval get_removed : unit -> int
Sourceval is_active : mode -> bool
Sourceval is_updating : mode -> bool
Sourceval cleanup_cache : unit -> unit
Sourcetype 'a digest = Why3Provers.t -> 'a -> string
Sourcetype 'a runner = timeout:float option -> steplimit:int option -> Why3Provers.t -> 'a -> VCS.result Frama_c_kernel.Task.task
Sourceval 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.

Sourceval get_result : digest:'a digest -> runner:'a runner -> 'a runner
Sourceval clear_result : digest:'a digest -> Why3Provers.t -> 'a -> unit