summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
authorSon HO2024-06-11 14:36:40 +0200
committerGitHub2024-06-11 14:36:40 +0200
commite60d525fe3dffa035d2a551af624747dca6e1c1e (patch)
treed7b06e270fd6a1cf69717f98db7c30e43788dad1 /tests/fstar
parent73e27b142b65ec37fbbc55a5a7d0299555b2b60b (diff)
parent2e91b90e332c473253c2ff91fd65da34eb709572 (diff)
Merge pull request #237 from AeneasVerif/son/tuples
Do not use tuple projectors in the Lean backend
Diffstat (limited to '')
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst29
1 files changed, 22 insertions, 7 deletions
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index a5ba31bc..f45d7f23 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -446,27 +446,42 @@ let read_then_incr (x : u32) : result (u32 & u32) =
Source: 'tests/src/no_nested_borrows.rs', lines 480:0-480:24 *)
type tuple_t (t1 t2 : Type0) = t1 * t2
-(** [no_nested_borrows::use_tuple_struct]:
- Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:48 *)
-let use_tuple_struct (x : tuple_t u32 u32) : result (tuple_t u32 u32) =
+(** [no_nested_borrows::read_tuple]:
+ Source: 'tests/src/no_nested_borrows.rs', lines 482:0-482:40 *)
+let read_tuple (x : (u32 & u32)) : result u32 =
+ let (i, _) = x in Ok i
+
+(** [no_nested_borrows::update_tuple]:
+ Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:39 *)
+let update_tuple (x : (u32 & u32)) : result (u32 & u32) =
+ let (_, i) = x in Ok (1, i)
+
+(** [no_nested_borrows::read_tuple_struct]:
+ Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:52 *)
+let read_tuple_struct (x : tuple_t u32 u32) : result u32 =
+ let (i, _) = x in Ok i
+
+(** [no_nested_borrows::update_tuple_struct]:
+ Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:51 *)
+let update_tuple_struct (x : tuple_t u32 u32) : result (tuple_t u32 u32) =
let (_, i) = x in Ok (1, i)
(** [no_nested_borrows::create_tuple_struct]:
- Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:61 *)
+ Source: 'tests/src/no_nested_borrows.rs', lines 498:0-498:61 *)
let create_tuple_struct (x : u32) (y : u64) : result (tuple_t u32 u64) =
Ok (x, y)
(** [no_nested_borrows::IdType]
- Source: 'tests/src/no_nested_borrows.rs', lines 491:0-491:20 *)
+ Source: 'tests/src/no_nested_borrows.rs', lines 503:0-503:20 *)
type idType_t (t : Type0) = t
(** [no_nested_borrows::use_id_type]:
- Source: 'tests/src/no_nested_borrows.rs', lines 493:0-493:40 *)
+ Source: 'tests/src/no_nested_borrows.rs', lines 505:0-505:40 *)
let use_id_type (t : Type0) (x : idType_t t) : result t =
Ok x
(** [no_nested_borrows::create_id_type]:
- Source: 'tests/src/no_nested_borrows.rs', lines 497:0-497:43 *)
+ Source: 'tests/src/no_nested_borrows.rs', lines 509:0-509:43 *)
let create_id_type (t : Type0) (x : t) : result (idType_t t) =
Ok x