Frama-C:
Plug-ins:
Libraries:

Frama-C API - ProofScript

class console : pool:Lang.F.pool -> title:string -> Wp__.Tactical.feedback
type jscript = alternative list
and 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
and 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;
}
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 jtactic : ?strategy:string -> Tactical.tactical -> Tactical.selection -> jtactic

Json Codecs

val json_of_selection : Tactical.selection -> Frama_c_kernel.Json.t
val selection_target : Frama_c_kernel.Json.t -> string
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