Module Wp.Wpo.VC_Annot

module VC_Annot: sig .. end

type t = {
   axioms : Wp.Definitions.axioms option;
   goal : Wp.Wpo.GOAL.t;
   tags : Wp.Splitter.tag list;
   warn : Wp.Warning.t list;
   deps : Property.Set.t;
   path : Cil_datatype.Stmt.Set.t;
   effect : (Cil_types.stmt * Wp.WpPropId.effect_source) option;
}
val is_trivial : t -> bool
val resolve : pid:Wp.WpPropId.prop_id -> t -> bool
val cache_descr : pid:Wp.WpPropId.prop_id ->
t -> (Wp.VCS.prover * Wp.VCS.result) list -> string