package ortac-runtime-qcheck-stm

  1. Overview
  2. Docs
Runtime support library for Ortac/QCheck-STM-generated code

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (5)

Authors

  1. N
    Nicolas Osborne <nicolas.osborne@tarides.com>
  2. N
    Nikolaus Huber <mail@n-huber.eu>

Maintainers

  1. N
    Nicolas Osborne <nicolas.osborne@tarides.com>

Sources

.tar.gz
md5=1bbffc8b2ecf943c2d66bdf9c72b994a
sha512=f23537bc18149e5cf5f5035139fac0541b55f7087127b1ca963f16d8852096d7fbdd5378b9fbb7703a3ce175b4a90ad8a7dfafc4292b5f1196fa11fbef43a178

doc/ortac-runtime-qcheck-stm.sequential/Ortac_runtime_qcheck_stm_sequential/index.html

Module Ortac_runtime_qcheck_stm_sequentialSource

include module type of struct include Ortac_runtime end
Sourcetype term_kind = Ortac_runtime.term_kind =
  1. | Check
  2. | Pre
  3. | Post
  4. | XPost
Sourcetype error = Ortac_runtime.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 = Ortac_runtime.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
Sourceexception Partial_function of exn * location
Sourceval string_of_integer : integer -> string
Sourceval copy : 'a -> 'a
Sourcemodule Gospelstdlib = Ortac_runtime.Gospelstdlib
module Report = Ortac_runtime_qcheck_stm_util.Report
module Model = Ortac_runtime_qcheck_stm_util.Stores.Model
module SUT = Ortac_runtime_qcheck_stm_util.Stores.SUT
Sourcemodule Make (Spec : STM.Spec) : sig ... end