summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/misc/External.Funs.fst16
1 files changed, 14 insertions, 2 deletions
diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst
index 3025da55..0ad40b00 100644
--- a/tests/misc/External.Funs.fst
+++ b/tests/misc/External.Funs.fst
@@ -11,7 +11,15 @@ include External.Opaque
let swap_fwd (t : Type0) (x : t) (y : t) (st : state) : result (state & unit) =
begin match core_mem_swap_fwd t x y st with
| Fail -> Fail
- | Return (st0, _) -> Return (st0, ())
+ | Return (st0, _) ->
+ begin match core_mem_swap_back0 t x y st with
+ | Fail -> Fail
+ | Return _ ->
+ begin match core_mem_swap_back1 t x y st with
+ | Fail -> Fail
+ | Return _ -> Return (st0, ())
+ end
+ end
end
(** [external::swap] *)
@@ -58,7 +66,11 @@ let custom_swap_fwd
| Return (st0, _) ->
begin match core_mem_swap_back0 t x y st with
| Fail -> Fail
- | Return x0 -> Return (st0, x0)
+ | Return x0 ->
+ begin match core_mem_swap_back1 t x y st with
+ | Fail -> Fail
+ | Return _ -> Return (st0, x0)
+ end
end
end