package frama-c

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Wpo.GOALSource

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

Innovation. Community. Security.