Module Wpo.VC_Annot

type t = {
axioms : Definitions.axioms option;
goal : GOAL.t;
tags : Splitter.tag list;
warn : Warning.t list;
deps : Frama_c_kernel.Property.Set.t;
path : Frama_c_kernel.Cil_datatype.Stmt.Set.t;
source : (Frama_c_kernel.Cil_types.stmt * Wp__Mcfg.goal_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