sig
type t
val get_id : VC.t -> string
val get_model : VC.t -> Model.t
val get_description : VC.t -> string
val get_property : VC.t -> Property.t
val get_result : VC.t -> VCS.prover -> VCS.result
val get_results : VC.t -> (VCS.prover * VCS.result) list
val get_logout : VC.t -> VCS.prover -> string
val get_logerr : VC.t -> VCS.prover -> string
val get_sequent : VC.t -> Conditions.sequent
val get_formula : VC.t -> Lang.F.pred
val is_trivial : VC.t -> bool
val is_proved : VC.t -> bool
val clear : unit -> unit
val proof : Property.t -> VC.t list
val remove : Property.t -> unit
val iter_ip : (VC.t -> unit) -> Property.t -> unit
val iter_kf :
(VC.t -> unit) -> ?bhv:string list -> Kernel_function.t -> unit
val generate_ip : ?model:string -> Property.t -> VC.t Bag.t
val generate_kf :
?model:string -> ?bhv:string list -> Kernel_function.t -> VC.t Bag.t
val generate_call : ?model:string -> Cil_types.stmt -> VC.t Bag.t
val prove :
VC.t ->
?config:VCS.config ->
?mode:VCS.mode ->
?start:(VC.t -> unit) ->
?callin:(VC.t -> VCS.prover -> unit) ->
?callback:(VC.t -> VCS.prover -> VCS.result -> unit) ->
VCS.prover -> bool Task.task
val spawn :
VC.t ->
?config:VCS.config ->
?start:(VC.t -> unit) ->
?callin:(VC.t -> VCS.prover -> unit) ->
?callback:(VC.t -> VCS.prover -> VCS.result -> unit) ->
?success:(VC.t -> VCS.prover option -> unit) ->
?pool:Task.pool -> (VCS.mode * VCS.prover) list -> unit
val server : ?procs:int -> unit -> Task.server
val command : VC.t Bag.t -> unit
end