Skip to content

Commit 7020dd3

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 b340e7f commit 7020dd3

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 = try Spec.run c sut with e -> Util.wrap_uncaught_exn Spec.show_cmd c e 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 = try Spec.run c sut with e -> Util.wrap_uncaught_exn Spec.show_cmd c e 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)