ocaml-gospel / ortac

Runtime assertion checking based on Gospel specifications
https://ocaml-gospel.github.io/ortac/
MIT License
36 stars 10 forks source link

Add support for exceptional behaviour to printing runnable scenario #206

Closed n-osborne closed 5 months ago

n-osborne commented 5 months ago

This PR proposes to add support for exceptional behaviour when printing a runnable scenariowhen a test is failing.

This PR is based on #204, please consider only the two last commits.

This PR should complete the story to fix #188

Again, if we introduce a bug in plugins/qcheck-stm/test/array.ml (here let get a _ = get a 7), we have now:

λ dune build @launchtests
File "plugins/qcheck-stm/test/dune.inc", line 49, characters 0-75:
49 | (rule
50 |  (alias launchtests)
51 |  (action
52 |   (run %{dep:array_stm_tests.exe} -v)))
random seed: 163835566
generated error fail pass / total     time test name
[✗]    1    0    1    0 / 1000     0.0s Array STM tests (generating)

--- Failure --------------------------------------------------------------------

Test Array STM tests failed (5 shrink steps):

   protect (fun () -> get sut (-952798241484687328))

+++ Messages ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Messages for test Array STM tests:

Gospel specification violation in function get

  File "array.mli", line 11, characters 11-26:
    0 <= i < t.size

when executing the following sequence of operations:

  open Array
  let protect f = try Ok (f ()) with e -> Error e
  let sut = make 16 'a'
  let r = protect (fun () -> get sut (-952798241484687328))
  assert (match r with
            | Error (Invalid_argument _) -> true
            | _ -> false)
  (* returned Ok ('a') *)

================================================================================
failure (1 tests failed, 0 tests errored, ran 1 tests)

[1]

So the call to any function that may raise an exception (according to the Gospel psecifications) are protected to return a ('a, exn) result instead of a simple 'a (as it is done today in QCheck-STM).

The value returned by the protected call is then compared to the expected result: here we were expecting an Invalid_argument exception because the clause is a checks, but in the case of a raises clause, the name of the expected exception will be printed.

Note that only the name of the exception is printed, this PR does not propose to handle the arguments of the said exception. I may want to wait to see how gospel#379 evolves.

n-osborne commented 5 months ago

I went for Either as reporting an exception here is not really an error (or it is in the same way as reporting a value).

I agree on having consistency on on the ocaml version :+1: