diff options
author | Sidney Congard | 2022-06-30 14:54:15 +0200 |
---|---|---|
committer | Sidney Congard | 2022-06-30 14:54:15 +0200 |
commit | fdbbb82ff89b1d5141ec63bc2385936da3de3616 (patch) | |
tree | d48e3fa933280e8a275d2cfdab8f126e920e5f13 /tests/misc/NoNestedBorrows.fst | |
parent | 47691de8fe3dc32a29663d4d8343eb415ce1d81e (diff) | |
parent | 4f33892c81cdaf6aefaad9b7cef1456dcfead67c (diff) |
Merge branch 'main' of github.com:Kachoc/aeneas into constants-v2
Complete the constants extraction by making all functions fail
Diffstat (limited to '')
-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] *) |