Skip to content

Commit

Permalink
STM: Print commands that trigger uncaught exceptions
Browse files Browse the repository at this point in the history
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 ()
```
  • Loading branch information
shym committed Jun 5, 2023
1 parent fb150c6 commit d997c94
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions lib/STM.ml
Original file line number Diff line number Diff line change
Expand Up @@ -170,15 +170,15 @@ struct
let rec interp_agree s sut cs = match cs with
| [] -> true
| c::cs ->
let res = Spec.run c sut in
let res = Util.tag_exn_with Spec.show_cmd (fun c -> Spec.run c sut) c in
let b = Spec.postcond c s res in
let s' = Spec.next_state c s in
b && interp_agree s' sut cs

let rec check_disagree s sut cs = match cs with
| [] -> None
| c::cs ->
let res = Spec.run c sut in
let res = Util.tag_exn_with Spec.show_cmd (fun c -> Spec.run c sut) c in
let b = Spec.postcond c s res in
let s' = Spec.next_state c s in
if b
Expand Down

0 comments on commit d997c94

Please sign in to comment.