package ortac-runtime-qcheck-stm

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Ortac_runtime_qcheck_stm`Source

include module type of Ortac_runtime

Sourcetype location = {

}

Sourcetype term_kind =

Sourcetype error =

| Violated_axiom
| Axiom_failure of {
1. exn : exn;
}
| Violated_invariant of {
1. term : string;
2. position : term_kind;
}
| Violated_condition of {
1. term : string;
2. term_kind : term_kind;
}
| Specification_failure of {
1. term : string;
2. term_kind : term_kind;
3. exn : exn;
}
| Unexpected_exception of {
1. allowed_exn : string list;
2. exn : exn;
}
| Uncaught_checks of {
1. term : string;
}
| Unexpected_checks of {
1. terms : string list;
}

Sourcetype error_report = {

}

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 =

| Value of STM.res
(*
The value has been computed
*)
| Protected_value of STM.res
(*
The value has been computed but is protected as it could have been an exception
*)
| Exception of string
(*
An exception is expected
*)
| 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

val 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