diff options
author | Son HO | 2022-09-22 18:52:15 +0200 |
---|---|---|
committer | GitHub | 2022-09-22 18:52:15 +0200 |
commit | dd75894c85bbaa5dc6aa54d39980e160e5b7777f (patch) | |
tree | ece56b01bcadea24a3c373236f0254f47e32a98f /tests/misc/NoNestedBorrows.fst | |
parent | d8f92140abd7e65b6f1c5dd7e511c0c0aa69e73f (diff) | |
parent | 0d5fb87166cc4eb4ddc783d871ad459479fc9fdc (diff) |
Merge pull request #1 from AeneasVerif/constants-v2
Implement support for globals
Diffstat (limited to 'tests/misc/NoNestedBorrows.fst')
-rw-r--r-- | tests/misc/NoNestedBorrows.fst | 28 |
1 files changed, 14 insertions, 14 deletions
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst index 35d32514..a694cff1 100644 --- a/tests/misc/NoNestedBorrows.fst +++ b/tests/misc/NoNestedBorrows.fst @@ -218,36 +218,36 @@ let _ = assert_norm (get_elem_test_fwd = Return ()) (** [no_nested_borrows::test_char] *) let test_char_fwd : result char = Return 'a' -(** [no_nested_borrows::Tree] *) -type tree_t (t : Type0) = -| TreeLeaf : t -> tree_t t -| TreeNode : t -> node_elem_t t -> tree_t t -> tree_t t - (** [no_nested_borrows::NodeElem] *) -and node_elem_t (t : Type0) = +type node_elem_t (t : Type0) = | NodeElemCons : tree_t t -> node_elem_t t -> node_elem_t t | NodeElemNil : node_elem_t t -(** [no_nested_borrows::even] *) -let rec even_fwd (x : u32) : result bool = +(** [no_nested_borrows::Tree] *) +and tree_t (t : Type0) = +| TreeLeaf : t -> tree_t t +| TreeNode : t -> node_elem_t t -> tree_t t -> tree_t t + +(** [no_nested_borrows::odd] *) +let rec odd_fwd (x : u32) : result bool = if x = 0 - then Return true + then Return false else begin match u32_sub x 1 with | Fail -> Fail | Return i -> - begin match odd_fwd i with | Fail -> Fail | Return b -> Return b end + begin match even_fwd i with | Fail -> Fail | Return b -> Return b end end -(** [no_nested_borrows::odd] *) -and odd_fwd (x : u32) : result bool = +(** [no_nested_borrows::even] *) +and even_fwd (x : u32) : result bool = if x = 0 - then Return false + then Return true else begin match u32_sub x 1 with | Fail -> Fail | Return i -> - begin match even_fwd i with | Fail -> Fail | Return b -> Return b end + begin match odd_fwd i with | Fail -> Fail | Return b -> Return b end end (** [no_nested_borrows::test_even_odd] *) |