module VC:sig
..end
type
t
val get_id : t -> string
val get_model : t -> WpContext.model
val get_scope : t -> WpContext.scope
val get_context : t -> WpContext.context
val get_description : t -> string
val get_property : t -> Property.t
val get_result : t -> VCS.prover -> VCS.result
val get_results : t -> (VCS.prover * VCS.result) list
val get_logout : t -> VCS.prover -> string
val get_logerr : t -> VCS.prover -> string
val get_sequent : t -> Conditions.sequent
val get_formula : t -> Lang.F.pred
val is_trivial : t -> bool
val is_proved : t -> bool
generate_xxx
functions below.val clear : unit -> unit
val proof : Property.t -> t list
val remove : Property.t -> unit
val iter_ip : (t -> unit) -> Property.t -> unit
val iter_kf : (t -> unit) -> ?bhv:string list -> Kernel_function.t -> unit
model
is what has been
given on the command line (-wp-model
option)val generate_ip : ?model:string -> Property.t -> t Bag.t
val generate_kf : ?model:string -> ?bhv:string list -> Kernel_function.t -> t Bag.t
val generate_call : ?model:string -> Cil_types.stmt -> t Bag.t
val prove : t ->
?config:VCS.config ->
?mode:VCS.mode ->
?start:(t -> unit) ->
?progress:(t -> string -> unit) ->
?result:(t -> VCS.prover -> VCS.result -> unit) ->
VCS.prover -> bool Task.task
val spawn : t ->
?config:VCS.config ->
?start:(t -> unit) ->
?progress:(t -> string -> unit) ->
?result:(t -> VCS.prover -> VCS.result -> unit) ->
?success:(t -> VCS.prover option -> unit) ->
?pool:Task.pool -> (VCS.mode * VCS.prover) list -> unit
prove
but schedule the tasks into the global server returned
by server
function below.
The first succeeding prover cancels the other ones.
val server : ?procs:int -> unit -> Task.server
-wp-par
command-line option.
The returned server is global to Frama-C, but the number of parallel task
allowed will be updated to fit the ~procs
or command-line options.val command : ?provers:Why3.Whyconf.prover list -> ?tip:bool -> t Bag.t -> unit
~provers
is set, it is used for computing the list of provers to spawn.
If ~tip
is set, it is used to compute the script execution mode.