Module `Wp.ProofScript`Source

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

Sourcetype jscript = alternative list

Sourceand 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

Sourceand jtactic = {

header : string;
tactic : string;
params : Frama_c_kernel.Json.t;
select : Frama_c_kernel.Json.t;
strategy : string option;

}

Sourceval is_prover : alternative -> bool

Sourceval is_tactic : alternative -> bool

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

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 decode : Frama_c_kernel.Json.t -> jscript

Sourceval encode : jscript -> Frama_c_kernel.Json.t

Source

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

Source

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

Json Codecs

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

Source

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

Sourceval selection_target : Frama_c_kernel.Json.t -> string

Source

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

Source

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

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

Source

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

Source

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

Sourceval json_of_result : VCS.prover -> VCS.result -> 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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/ProofScript/index.html

Module `Wp.ProofScript`Source

package frama-c

Install

Dune Dependency

Authors

Maintainers

Sources

doc/frama-c-wp.core/Wp/ProofScript/index.html

Module Wp.ProofScriptSource

Module `Wp.ProofScript`Source