5 files changed, 79 insertions, 0 deletions

diff --git a/tests/src/loops-borrow-check-fail.borrow-check.out b/tests/src/loops-borrow-check-fail.borrow-check.out
new file mode 100644
index 00000000..54bb2102
--- /dev/null
+++ b/tests/src/loops-borrow-check-fail.borrow-check.out
@@ -0,0 +1,17 @@
+[Info ] Imported: tests/llbc/loops_borrow_check_fail.llbc
+[Error] Inconsistent projection:
+- pe: Expressions.Deref
+- v:
+Values.VBottom
+- ty:
+(Types.TRef (Types.RErased, (Types.TLiteral (Values.TInteger Values.I32)),
+   Types.RMut))
+Source: 'tests/src/loops-borrow-check-fail.rs', lines 7:4-12:1
+[Error] Inconsistent projection:
+- pe: Expressions.Deref
+- v:
+Values.VBottom
+- ty:
+(Types.TRef (Types.RErased, (Types.TLiteral (Values.TInteger Values.I32)),
+   Types.RShared))
+Source: 'tests/src/loops-borrow-check-fail.rs', lines 17:4-21:1
diff --git a/tests/src/loops-borrow-check-fail.rs b/tests/src/loops-borrow-check-fail.rs
new file mode 100644
index 00000000..24be052c
--- /dev/null
+++ b/tests/src/loops-borrow-check-fail.rs
@@ -0,0 +1,21 @@
+//@ [!borrow-check] skip
+//@ [borrow-check] known-failure
+
+// We need to use the general rules for joining the loans
+fn loop_reborrow_mut() {
+    let mut x = 0;
+    let mut px = &mut x;
+    while *px > 0 {
+        x += 1;
+        px = &mut x;
+    }
+}
+
+// We need to imrpove [prepare_ashared_loans]
+fn iter_local_shared_borrow() {
+    let mut x = 0;
+    let mut p = &x;
+    loop {
+        p = &(*p);
+    }
+}
diff --git a/tests/src/loops-borrow-check-negative.borrow-check.out b/tests/src/loops-borrow-check-negative.borrow-check.out
new file mode 100644
index 00000000..093d8b8a
--- /dev/null
+++ b/tests/src/loops-borrow-check-negative.borrow-check.out
@@ -0,0 +1,3 @@
+[Info ] Imported: tests/llbc/loops_borrow_check_negative.llbc
+[Error] Can't end abstraction 16 as it is set as non-endable
+Source: 'tests/src/loops-borrow-check-negative.rs', lines 18:0-18:66
diff --git a/tests/src/loops-borrow-check-negative.rs b/tests/src/loops-borrow-check-negative.rs
new file mode 100644
index 00000000..3386d581
--- /dev/null
+++ b/tests/src/loops-borrow-check-negative.rs
@@ -0,0 +1,28 @@
+//@ [!borrow-check] skip
+//@ [borrow-check] known-failure
+
+// This succeeds
+fn loop_a<'a>(a: &'a mut u32, b: &'a mut u32) -> &'a mut u32 {
+    let mut x = 0;
+    while x > 0 {
+        x += 1;
+    }
+    if x > 0 {
+        a
+    } else {
+        b
+    }
+}
+
+// This fails
+fn loop_a_b<'a, 'b>(a: &'a mut u32, b: &'b mut u32) -> &'a mut u32 {
+    let mut x = 0;
+    while x > 0 {
+        x += 1;
+    }
+    if x > 0 {
+        a
+    } else {
+        b // Expect lifetime 'a
+    }
+}
diff --git a/tests/src/loops-borrow-check.rs b/tests/src/loops-borrow-check.rs
new file mode 100644
index 00000000..ab300b37
--- /dev/null
+++ b/tests/src/loops-borrow-check.rs
@@ -0,0 +1,10 @@
+//@ [!borrow-check] skip
+
+fn iter_local_mut_borrow() {
+    let mut x = 0;
+    let mut p = &mut x;
+    loop {
+        p = &mut (*p);
+        *p += 1;
+    }
+}