diff options
| author | Pierre-Marie Pédrot | 2015-05-18 17:47:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-18 19:04:32 +0200 |
| commit | ea3909466eaaf86ff212c0a002e5df11e4a979f5 (patch) | |
| tree | 2fd23c2ffa95c3bcfcd5c3e15404716dbc4df283 /lib/errors.ml | |
| parent | b994685d85d30f0db8ee0ec10f802f6bf3797e4b (diff) | |
The Fail command does not catch uncaught exception anomalies anymore.
Diffstat (limited to 'lib/errors.ml')
| -rw-r--r-- | lib/errors.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/lib/errors.ml b/lib/errors.ml index 999d99ee08..c60442654a 100644 --- a/lib/errors.ml +++ b/lib/errors.ml @@ -120,3 +120,12 @@ let noncritical = function | Timeout | Drop | Quit -> false | Invalid_argument "equal: functional value" -> false | _ -> true + +(** Check whether an exception is handled *) + +exception Bottom + +let handled e = + let bottom _ = raise Bottom in + try let _ = print_gen bottom !handle_stack e in true + with Bottom -> false |