ProofStrategy (frama-c-wp.Wp.ProofStrategy)

type strategy

type alternative

val typecheck : unit -> unit

val name : strategy -> string

val loc : strategy -> Frama_c_kernel.Cil_types.location

val find : string -> strategy option

val hints : ?node:ProofEngine.node -> Wpo.t -> strategy list

val has_hint : Wpo.t -> bool

val iter : (strategy -> unit) -> unit

val default : unit -> strategy list

val alternatives : strategy -> alternative list

val provers : 
  ?default:VCS.prover list ->
  alternative ->
  VCS.prover list * float

val auto : alternative -> Strategy.heuristic option

val fallback : alternative -> strategy option

val tactic : 
  ProofEngine.tree ->
  ProofEngine.node ->
  strategy ->
  alternative ->
  ProofEngine.node list option

val pp_strategy : Stdlib.Format.formatter -> strategy -> unit

val pp_alternative : Stdlib.Format.formatter -> alternative -> unit