ocaml-gospel / ortac

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

Add a Partial_specification exception to the runtime and use it in the QCheck-STM plugin #157

Closed shym closed 11 months ago

shym commented 11 months ago

This PR improves the error message when partial functions of the runtime, ie the ones that can raise exceptions at execution time, are called out of their definition domain in the QCheck-STM plugin.

For instance, running into a List.hd [] during the test run will now display something like:

exception Partial function in specification
File "array.mli", line 40, characters 12-26:
A partial function used in the specification was called out of its definition
domain, raising the following exception:
Failure("hd")

which points to the clause where the Failure was raised.

This PR thus adds:

Hopefully this improves #150.

shym commented 11 months ago

Closes #153.

shym commented 11 months ago

I think I would rather call the new exception Partial_function than Partial_specification as the second can be a bit misleading.

Indeed, in the message I wrote “Partial function in a spec...”, I don’t know why I went for something different in the name... :sweat_smile:

There are some Ortac/QCheck-STM specifics in the addition to ortac-core, but I guess that can be generalized in the future if it need to be.

My feeling was that the function term_with_catch is currently used only by Ortac/QCheck-STM, but not really specific to it, which is why I placed it there. Wrapper contains a function fairly similar, it might be possible to rewrite them so that they share it.