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

class console : pool:Lang.F.pool -> title:string -> Wp__.Tactical.feedback

type jscript = alternative list

and alternative = private

| Prover of VCS.prover * VCS.result
| Tactic of int * jtactic * (string * jscript) list
(*
With number of pending goals
*)
| Error of string * Frama_c_kernel.Json.t

and jtactic = {

}

val is_prover : alternative -> bool

val is_tactic : alternative -> bool

val a_prover : VCS.prover -> VCS.result -> alternative

val a_tactic : jtactic -> (string * jscript) list -> alternative

val pending : alternative -> int

pending goals

val pending_any : jscript -> int

minimum of pending goals

val has_proof : jscript -> bool

Has a tactical alternative

val decode : Frama_c_kernel.Json.t -> jscript

val encode : jscript -> Frama_c_kernel.Json.t

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

val configure : 
  jtactic ->
  Conditions.sequent ->
  (Tactical.tactical * Tactical.selection) option

Json Codecs

val json_of_selection : Tactical.selection -> Frama_c_kernel.Json.t

val selection_of_json : 
  Conditions.sequent ->
  Frama_c_kernel.Json.t ->
  Tactical.selection

val selection_target : Frama_c_kernel.Json.t -> string

val json_of_param : 
  Tactical.tactical ->
  Tactical.parameter ->
  string * Frama_c_kernel.Json.t

val param_of_json : 
  Tactical.tactical ->
  Conditions.sequent ->
  Frama_c_kernel.Json.t ->
  Tactical.parameter ->
  unit

val json_of_parameters : Tactical.tactical -> Frama_c_kernel.Json.t

val parameters_of_json : 
  Tactical.tactical ->
  Conditions.sequent ->
  Frama_c_kernel.Json.t ->
  unit

val json_of_tactic : 
  jtactic ->
  (string * Frama_c_kernel.Json.t) list ->
  Frama_c_kernel.Json.t

val json_of_result : VCS.prover -> VCS.result -> Frama_c_kernel.Json.t

val prover_of_json : Frama_c_kernel.Json.t -> VCS.prover option

val result_of_json : Frama_c_kernel.Json.t -> VCS.result