Module Ortac_runtime_qcheck_stm_util.Report

type 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.

type t = {
  1. mod_name : string;
    (*

    The name of the module under test

    *)
  2. init_sut : string;
    (*

    String representation of the init_sut function

    *)
  3. exp_res : expected_result;
    (*

    The expected result of the call

    *)
  4. cmd : string;
    (*

    String representation of the call

    *)
  5. terms : (string * Ortac_runtime.location) list;
    (*

    String representation and location of the violated specifications

    *)
}

Information for the bug report in case of test failure

type trace = {
  1. call : string;
  2. res : STM.res;
}
val report : string -> string -> expected_result -> string -> (string * Ortac_runtime.location) list -> t

report module_name init_sut exp_res cmd terms

val append : t option -> t option -> t option

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

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

A dummy STM.res for unknown returned values

val is_dummy : STM.res -> bool
val pp_expected_result : expected_result Fmt.t
val pp_terms : (string * Ortac_runtime.location) list Fmt.t
val pp_traces : bool -> expected_result -> trace list Fmt.t
val message : ('a * t) Fmt.t -> 'a -> t -> 'b