Module Wp.ProofScriptSource

Sourceclass console : pool:Lang.F.pool -> title:string -> Wp__.Tactical.feedback
Sourcetype jscript = alternative list
Sourceand alternative = private
  1. | Prover of VCS.prover * VCS.result
  2. | Tactic of int * jtactic * (string * jscript) list
    (*

    With number of pending goals

    *)
  3. | Error of string * Frama_c_kernel.Json.t
Sourceand jtactic = {
  1. header : string;
  2. tactic : string;
  3. params : Frama_c_kernel.Json.t;
  4. select : Frama_c_kernel.Json.t;
  5. strategy : string option;
}
Sourceval is_prover : alternative -> bool
Sourceval is_tactic : alternative -> bool
Sourceval a_tactic : jtactic -> (string * jscript) list -> alternative
Sourceval pending : alternative -> int

pending goals

Sourceval pending_any : jscript -> int

minimum of pending goals

Sourceval has_proof : jscript -> bool

Has a tactical alternative

Sourceval jtactic : ?strategy:string -> Tactical.tactical -> Tactical.selection -> jtactic

Json Codecs

Sourceval selection_target : Frama_c_kernel.Json.t -> string
Sourceval json_of_tactic : jtactic -> (string * Frama_c_kernel.Json.t) list -> Frama_c_kernel.Json.t
Sourceval prover_of_json : Frama_c_kernel.Json.t -> VCS.prover option
Sourceval result_of_json : Frama_c_kernel.Json.t -> VCS.result