Module Vc

module Vc: sig .. end

WhyML VC generators

val sp_attr : Why3.Ident.attribute

val wp_attr : Why3.Ident.attribute

val kp_attr : Why3.Ident.attribute

val wb_attr : Why3.Ident.attribute

val nt_attr : Why3.Ident.attribute

val set_infer_invs : (Why3.Ident.Sattr.t ->
        Why3.Env.env ->
        Why3.Decl.known_map ->
        Why3.Pdecl.known_map ->
        Why3.Expr.expr -> Why3.Ity.cty -> (Why3.Expr.expr * Why3.Term.term) list) ->
       unit

val warn_missing_diverges : Why3.Loc.warning_id

val vc : Why3.Env.env ->
       Why3.Pdecl.known_map ->
       Why3.Theory.theory_uc -> Why3.Pdecl.pdecl -> Why3.Pdecl.pdecl list