Frama-C:
Plug-ins:
Libraries:

Frama-C API - ProofStrategy

type 'a loc = {
  1. loc : Frama_c_kernel.Cil_types.location;
  2. value : 'a;
}
type strategy = {
  1. name : string loc;
  2. alternatives : alternative loc list;
}
and 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;
}
and 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
type context
val debug_table : context -> (string, Wp__.Pattern.pattern) Frama_c_kernel.Hashtbl.t
val parse_alternatives : context -> Frama_c_kernel.Logic_ptree.lexpr list -> alternative loc list
val typecheck : ?env:Wp__.Pattern.env -> unit -> unit
val typecheck_strategy : Wp__.Pattern.env -> string loc -> unit
val typecheck_prover : Wp__.Pattern.env -> string loc -> unit
val typecheck_auto : Wp__.Pattern.env -> string loc -> unit
val typecheck_tactic : Wp__.Pattern.env -> tactic -> unit
val name : strategy -> string
val find : string -> strategy option
val hints : ?node:ProofEngine.node -> Wpo.t -> strategy list
val has_hint : Wpo.t -> bool
val tactical : string loc -> Tactical.tactical
val select : Wp__.Pattern.sigma -> ?goal:Lang.F.pred -> Wp__.Pattern.value list -> Tactical.selection
val configure : Wp__.Pattern.env -> Tactical.tactical -> Wp__.Pattern.sigma -> (string loc * Wp__.Pattern.value) -> unit
val iter : (strategy -> unit) -> unit
val default : unit -> strategy list
val alternatives : strategy -> alternative loc list
val provers : ?default:VCS.prover list -> alternative loc -> VCS.prover list * float
val auto : alternative loc -> Strategy.heuristic option
val fallback : alternative loc -> strategy option
val pp_strategy : Stdlib.Format.formatter -> strategy -> unit
val pp_alternative : Stdlib.Format.formatter -> alternative loc -> unit