Frama-C API - VC
WP Proof Obligation Generator and Management
Proof Obligations
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
.
Database
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
Generators
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
Prover Interface
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.