package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type prover_answer =
  1. | Valid
  2. | Invalid
  3. | Timeout
  4. | OutOfMemory
  5. | StepLimitExceeded
  6. | Unknown of string
  7. | Failure of string
  8. | HighFailure
type prover_result = {
  1. pr_answer : prover_answer;
  2. pr_status : Unix.process_status;
  3. pr_output : string;
  4. pr_time : float;
  5. pr_steps : int;
  6. pr_model : Model_parser.model;
}
val print_prover_answer : Format.formatter -> prover_answer -> unit
val print_prover_result : json_model:bool -> Format.formatter -> prover_result -> unit
val debug : Debug.flag
type timeregexp
type stepregexp
val timeregexp : string -> timeregexp
val stepregexp : string -> int -> stepregexp
type prover_result_parser = {
  1. prp_regexps : (string * prover_answer) list;
  2. prp_timeregexps : timeregexp list;
  3. prp_stepregexps : stepregexp list;
  4. prp_exitcodes : (int * prover_answer) list;
  5. prp_model_parser : Model_parser.model_parser;
}
type prover_call
type resource_limit = {
  1. limit_time : int;
  2. limit_mem : int;
  3. limit_steps : int;
}
val empty_limit : resource_limit
val call_editor : command:string -> string -> prover_call
val call_on_buffer : command:string -> limit:resource_limit -> res_parser:prover_result_parser -> filename:string -> printer_mapping:Printer.printer_mapping -> gen_new_file:bool -> ?inplace:bool -> Buffer.t -> prover_call
type prover_update =
  1. | NoUpdates
  2. | ProverInterrupted
  3. | InternalFailure of exn
  4. | ProverStarted
  5. | ProverFinished of prover_result
val get_new_results : blocking:bool -> (prover_call * prover_update) list
val query_call : prover_call -> prover_update
val interrupt_call : prover_call -> unit
val wait_on_call : prover_call -> prover_result
OCaml

Innovation. Community. Security.