Ortac_runtime_qcheck_stm
include module type of Ortac_runtime
type error =
| Violated_axiom
| Axiom_failure of {
}
| Violated_invariant of {
term : string;
position : term_kind;
}
| Violated_condition of {
term : string;
term_kind : term_kind;
}
| Specification_failure of {
term : string;
term_kind : term_kind;
exn : exn;
}
| Unexpected_exception of {
}
| Uncaught_checks of {
}
| Unexpected_checks of {
}
val pp_loc : Stdlib.Format.formatter -> location -> unit
val pp_error_report : Stdlib.Format.formatter -> error_report -> unit
exception Error of error_report
module Errors : sig ... end
exception Partial_function of exn * location
val string_of_integer : integer -> string
module Gospelstdlib : sig ... end
module Z : sig ... end
type 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.
val report :
string ->
string ->
expected_result ->
string ->
(string * location) list ->
report
report module_name init_sut ret cmd terms
append a b
appends the violated terms of a
and b
if any in the returned report
module Model : sig ... end
module SUT : sig ... end