sig
type t = {
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 repr : Wpo.VC_Annot.t
val resolve : Wpo.VC_Annot.t -> bool
val is_trivial : Wpo.VC_Annot.t -> bool
val pp_effect :
Format.formatter ->
(Cil_datatype.Stmt.t * WpPropId.effect_source) option -> unit
val pretty :
Format.formatter ->
WpPropId.prop_id ->
Wpo.VC_Annot.t -> (VCS.prover * VCS.result) list -> unit
val cache_descr :
pid:WpPropId.prop_id ->
Wpo.VC_Annot.t -> (VCS.prover * VCS.result) list -> string
end