sig
module Wpo :
sig
type prover
type result
type po
val file_for_log_proof :
Dynamic_plugins.Wp.Wpo.po ->
Dynamic_plugins.Wp.Wpo.prover -> string * string
val prover_of_name : string -> Dynamic_plugins.Wp.Wpo.prover option
val iter_on_goals : (Dynamic_plugins.Wp.Wpo.po -> unit) -> unit
val is_valid : Dynamic_plugins.Wp.Wpo.result -> bool
val goals_of_property : Property.t -> Dynamic_plugins.Wp.Wpo.po list
val get_result :
Dynamic_plugins.Wp.Wpo.po ->
Dynamic_plugins.Wp.Wpo.prover -> Dynamic_plugins.Wp.Wpo.result
val get_gid : Dynamic_plugins.Wp.Wpo.po -> string
val get_property : Dynamic_plugins.Wp.Wpo.po -> Property.t
end
val wp_compute_kf :
Cil_datatype.Kf.t option -> string list -> string list -> unit
val wp_clear_session : unit -> unit
val wp_iter_session : (Dynamic_plugins.Wp.Wpo.po -> unit) -> unit
val wp_compute :
Cil_datatype.Kf.t option -> string list -> Property.t option -> unit
val wp_end_session : unit -> unit
val wp_compute_call : Cil_datatype.Stmt.t -> unit
val run : unit -> unit
val wp_clear : unit -> unit
val wp_begin_session : unit -> unit
val wp_compute_ip : Property.t -> unit
end