package frama-c

You can search for identifiers within the package.

in-package search v0.2.0

Module `Wp.ProofStrategy`Source

Sourcetype strategy

Sourcetype alternative

Sourceval typecheck : unit -> unit

Sourceval name : strategy -> string

Sourceval loc : strategy -> Frama_c_kernel.Cil_types.location

Sourceval find : string -> strategy option

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

Sourceval has_hint : Wpo.t -> bool

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

Sourceval default : unit -> strategy list

Sourceval alternatives : strategy -> alternative list

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

Sourceval auto : alternative -> Strategy.heuristic option

Sourceval fallback : alternative -> strategy option

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

Sourceval pp_strategy : Format.formatter -> strategy -> unit

Sourceval pp_alternative : Format.formatter -> alternative -> unit