package ortac-runtime-qcheck-stm

You can search for identifiers within the package.

in-package search v0.2.0

Runtime support library for Ortac/QCheck-STM-generated code

Install

Dune Dependency

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

Authors

Maintainers

N

Nicolas Osborne <nicolas.osborne@tarides.com>

Sources

0.7.0.tar.gz

md5=1429cb7ec517060772f97504d84ff789

sha512=498e1b40dd29f5feef3df5fa54f924c7b53f24726b1613a5d8dd7ef8ca16b8cf97a76b9fd2951f32143b59a67b8d80fe13b081890fca07787a5a5fda30102a97

doc/ortac-runtime-qcheck-stm/Ortac_runtime_qcheck_stm/index.html

Module `Ortac_runtime_qcheck_stm`Source

include module type of Ortac_runtime

Sourcetype location = {

start : Lexing.position;
stop : Lexing.position;

}

Sourcetype term_kind =

| Check
| Pre
| Post
| XPost

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 = {

loc : location;
fun_name : string;
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 =

| 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

Source

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