Skip to content

Commit bebbbed

Browse files
committed
STM: Print commands that trigger uncaught exceptions
The standard QCheck mechanism to catch exceptions that are raised in tests do not give much clue about the source (ie STM command) of that exception This packs the unsoundly-specified command with the exception in such a case so that it can be displayed Before: ``` exception Failure("unexpected") ``` After: ``` exception Failure("unexpected") raised but not caught while running AlwaysFail () ```
1 parent c9c70c9 commit bebbbed

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

lib/STM.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -170,15 +170,15 @@ struct
170170
let rec interp_agree s sut cs = match cs with
171171
| [] -> true
172172
| c::cs ->
173-
let res = Spec.run c sut in
173+
let res = Util.tag_exn_with Spec.show_cmd (fun c -> Spec.run c sut) c in
174174
let b = Spec.postcond c s res in
175175
let s' = Spec.next_state c s in
176176
b && interp_agree s' sut cs
177177

178178
let rec check_disagree s sut cs = match cs with
179179
| [] -> None
180180
| c::cs ->
181-
let res = Spec.run c sut in
181+
let res = Util.tag_exn_with Spec.show_cmd (fun c -> Spec.run c sut) c in
182182
let b = Spec.postcond c s res in
183183
let s' = Spec.next_state c s in
184184
if b

0 commit comments

Comments
 (0)