Frama-C:
Plug-ins:
Libraries:

Frama-C API - GOAL

type t
val dummy : t
val trivial : t
val is_trivial : t -> bool
val is_computed : t -> bool
val make : Conditions.sequent -> t
val compute : pid:WpPropId.prop_id -> t -> unit
val compute_proof : pid:WpPropId.prop_id -> ?opened:bool -> t -> Lang.F.pred
val compute_descr : pid:WpPropId.prop_id -> t -> Conditions.sequent
val compute_probes : pid:WpPropId.prop_id -> t -> Lang.F.term Wp__.Probe.Map.t
val get_descr : t -> Conditions.sequent
val qed_time : t -> float