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