summaryrefslogtreecommitdiff
path: root/tests/src
diff options
context:
space:
mode:
authorSon HO2024-06-11 14:36:40 +0200
committerGitHub2024-06-11 14:36:40 +0200
commite60d525fe3dffa035d2a551af624747dca6e1c1e (patch)
treed7b06e270fd6a1cf69717f98db7c30e43788dad1 /tests/src
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/src/no_nested_borrows.rs14
1 files changed, 13 insertions, 1 deletions
diff --git a/tests/src/no_nested_borrows.rs b/tests/src/no_nested_borrows.rs
index 11c4a695..20f8efea 100644
--- a/tests/src/no_nested_borrows.rs
+++ b/tests/src/no_nested_borrows.rs
@@ -479,7 +479,19 @@ pub fn read_then_incr(x: &mut u32) -> u32 {
pub struct Tuple<T1, T2>(T1, T2);
-pub fn use_tuple_struct(x: &mut Tuple<u32, u32>) {
+pub fn read_tuple(x: &(u32, u32)) -> u32 {
+ x.0
+}
+
+pub fn update_tuple(x: &mut (u32, u32)) {
+ x.0 = 1;
+}
+
+pub fn read_tuple_struct(x: &Tuple<u32, u32>) -> u32 {
+ x.0
+}
+
+pub fn update_tuple_struct(x: &mut Tuple<u32, u32>) {
x.0 = 1;
}