Module Wpo.VC_Annot

module VC_Annot: sig .. end

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