summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorBrian Campbell2019-06-03 18:31:53 +0100
committerBrian Campbell2019-06-03 18:31:53 +0100
commit15d455f388075db4dcccb5c348e9cd725124b318 (patch)
tree5f35e3aca492c5844f1fac490e56d9f0cc55fec0
parentd076ac77dfbb4ff683bc57cb58c52f497f0e4618 (diff)
Test case for previous commit
-rw-r--r--test/coq/pass/non_exh_exc.sail18
1 files changed, 18 insertions, 0 deletions
diff --git a/test/coq/pass/non_exh_exc.sail b/test/coq/pass/non_exh_exc.sail
new file mode 100644
index 00000000..8ce99163
--- /dev/null
+++ b/test/coq/pass/non_exh_exc.sail
@@ -0,0 +1,18 @@
+default Order dec
+$include <prelude.sail>
+
+union exception = {
+ Error_foo : unit,
+ Error_bar : int
+}
+
+val f : int -> int effect {escape}
+
+function f(n) = {
+ try {
+ let m : int = if n > 5 then n - 3 else throw(Error_bar(n)) in
+ m + 1
+ } catch {
+ Error_bar(n) => n
+ }
+}