Wp.VC
WP Proof Obligation Generator and Management
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 -> Frama_c_kernel.Property.t
val get_result : t -> VCS.prover -> VCS.result
val get_results : t -> (VCS.prover * VCS.result) list
val get_sequent : t -> Conditions.sequent
val get_formula : t -> Lang.F.pred
val is_trivial : t -> bool
val is_valid : t -> bool
One prover at least returns a valid verdict.
val has_unknown : t -> bool
At least one non-valid verdict.
val is_passed : t -> bool
Same as is_valid
for non-smoke tests. For smoke-tests, same as is_unknown
.
Notice that a property or a function have no proof obligation until you explicitly generate them via the generate_xxx
functions below.
val proof : Frama_c_kernel.Property.t -> t list
List of proof obligations computed for a given property. Might be empty if you don't have used one of the generators below.
val remove : Frama_c_kernel.Property.t -> unit
val iter_ip : (t -> unit) -> Frama_c_kernel.Property.t -> unit
val iter_kf :
(t -> unit) ->
?bhv:string list ->
Frama_c_kernel.Kernel_function.t ->
unit
The generated VCs are also added to the database, so they can be accessed later. The default value for model
is what has been given on the command line (-wp-model
option)
val generate_ip :
?model:string ->
Frama_c_kernel.Property.t ->
t Frama_c_kernel.Bag.t
val generate_kf :
?model:string ->
?bhv:string list ->
?prop:string list ->
Frama_c_kernel.Kernel_function.t ->
t Frama_c_kernel.Bag.t
val generate_call :
?model:string ->
Frama_c_kernel.Cil_types.stmt ->
t Frama_c_kernel.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 Frama_c_kernel.Task.task
Returns a ready-to-schedule 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:Frama_c_kernel.Task.pool ->
(VCS.mode * VCS.prover) list ->
unit
Same as 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 -> Frama_c_kernel.Task.server
Default number of parallel tasks is given by -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 Frama_c_kernel.Bag.t ->
unit
Run the provers with the command-line interface. If ~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.