[qcheck-stm] Incorrect runnable scenario on normal behaviour when function could have raised an exception

[n-osborne]

To reproduce add the following declaration to plugins/qcheck-stm/test/array.ml:

let get a i = get a (i+1)

dune build @launchtests will give you something like:

Messages for test Array STM tests:

Gospel specification violation in function get

  File "array.mli", line 13, characters 12-37:
    a = List.nth t.contents i

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 _ = protect (fun () -> fill sut 3 5 '\219')
  (* returned Ok (()) *)
  let r = protect (fun () -> get sut 2)
  assert (r = 'a')
  (* returned Ok ('\219') *)

We would have expected:

assert (r = Ok 'a')

[n-osborne]

The generated code doesn't tell the runtime when a returned value could have been an exception.

Back in the days, I used (string, res) either type to encode whether it is an exception or a value, but in fact, we need three cases:

• value from a function without exceptional behaviour
• value from a function with an exceptional behaviour
• exception

And then adapt pp_expected accordingly