package ortac-runtime-qcheck-stm

  1. Overview
  2. Docs

Module Ortac_runtime_qcheck_stmSource

include module type of Ortac_runtime
Sourcetype location = {
  1. start : Lexing.position;
  2. stop : Lexing.position;
}
Sourcetype term_kind =
  1. | Check
  2. | Pre
  3. | Post
  4. | XPost
Sourcetype error =
  1. | Violated_axiom
  2. | Axiom_failure of {
    1. exn : exn;
    }
  3. | Violated_invariant of {
    1. term : string;
    2. position : term_kind;
    }
  4. | Violated_condition of {
    1. term : string;
    2. term_kind : term_kind;
    }
  5. | Specification_failure of {
    1. term : string;
    2. term_kind : term_kind;
    3. exn : exn;
    }
  6. | Unexpected_exception of {
    1. allowed_exn : string list;
    2. exn : exn;
    }
  7. | Uncaught_checks of {
    1. term : string;
    }
  8. | Unexpected_checks of {
    1. terms : string list;
    }
Sourcetype error_report = {
  1. loc : location;
  2. fun_name : string;
  3. mutable errors : error list;
}
Sourceval pp_loc : Format.formatter -> location -> unit
Sourceval pp_error_report : Format.formatter -> error_report -> unit
Sourceexception Error of error_report
Sourcemodule Errors : sig ... end
Sourceexception Partial_function of exn * location
Sourcetype integer
Sourceval string_of_integer : integer -> string
Sourceval copy : 'a -> 'a
Sourcemodule Gospelstdlib : sig ... end
Sourcemodule Z : sig ... end
Sourcetype expected_result =
  1. | Value of STM.res
    (*

    The value has been computed

    *)
  2. | Protected_value of STM.res
    (*

    The value has been computed but is protected as it could have been an exception

    *)
  3. | Exception of string
    (*

    An exception is expected

    *)
  4. | Out_of_domain
    (*

    The computation of the expected returned value called a Gospel function out of its domain

    *)

This type carries the expected value computed from the Gospel specification if possible.

Sourcetype report

Information for the bug report in case of test failure

Sourceval report : string -> string -> expected_result -> string -> (string * location) list -> report

report module_name init_sut ret cmd terms

Sourceval append : report option -> report option -> report option

append a b appends the violated terms of a and b if any in the returned report

Sourceval dummy : 'a STM.ty * ('b -> string)

A dummy STM.res for unknown returned values

Sourcemodule Model : sig ... end
Sourcemodule SUT : sig ... end
Sourcemodule Make (Spec : STM.Spec) : sig ... end