module VC_Annot:sig
..end
type
t = {
|
goal : |
|
: |
|
warn : |
|
deps : |
|
path : |
|
effect : |
val repr : t
val resolve : t -> bool
val is_trivial : t -> bool
val pp_effect : Format.formatter ->
(Cil_datatype.Stmt.t * WpPropId.effect_source) option -> unit
val pretty : Format.formatter ->
WpPropId.prop_id -> t -> (VCS.prover * VCS.result) list -> unit
val cache_descr : pid:WpPropId.prop_id ->
t -> (VCS.prover * VCS.result) list -> string