Module Wp.ProofStrategySource

Sourcetype 'a loc = {
  1. loc : Frama_c_kernel.Cil_types.location;
  2. value : 'a;
}
Sourcetype strategy = {
  1. name : string loc;
  2. alternatives : alternative loc list;
}
Sourceand tactic = {
  1. tactic : string loc;
  2. lookup : Wp__.Pattern.lookup list;
  3. select : Wp__.Pattern.value list;
  4. params : (string loc * Wp__.Pattern.value) list;
  5. children : (string loc * string loc) list;
  6. default : string loc option;
}
Sourceand alternative =
  1. | Default
  2. | Strategy of string loc
  3. | Provers of string loc list * float option
  4. | Auto of string loc
  5. | Tactic of tactic
Sourcetype context
Sourceval debug_table : context -> (string, Wp__.Pattern.pattern) Frama_c_kernel.Hashtbl.t
Sourceval parse_alternatives : context -> Frama_c_kernel.Logic_ptree.lexpr list -> alternative loc list
Sourceval typecheck : unit -> unit
Sourceval typecheck_strategy : Wp__.Pattern.env -> string loc -> unit
Sourceval typecheck_prover : Wp__.Pattern.env -> string loc -> unit
Sourceval typecheck_auto : Wp__.Pattern.env -> string loc -> unit
Sourceval typecheck_tactic : Wp__.Pattern.env -> tactic -> unit
Sourceval name : strategy -> string
Sourceval find : string -> strategy option
Sourceval hints : ?node:ProofEngine.node -> Wpo.t -> strategy list
Sourceval has_hint : Wpo.t -> bool
Sourceval tactical : string loc -> Tactical.tactical
Sourceval select : Wp__.Pattern.sigma -> ?goal:Lang.F.pred -> Wp__.Pattern.value list -> Tactical.selection
Sourceval configure : Wp__.Pattern.env -> Tactical.tactical -> Wp__.Pattern.sigma -> (string loc * Wp__.Pattern.value) -> unit
Sourceval iter : (strategy -> unit) -> unit
Sourceval default : unit -> strategy list
Sourceval alternatives : strategy -> alternative loc list
Sourceval provers : ?default:Prover.t list -> alternative loc -> Prover.t list * float
Sourceval fallback : alternative loc -> strategy option
Sourceval pp_strategy : Format.formatter -> strategy -> unit
Sourceval pp_alternative : Format.formatter -> alternative loc -> unit