Merge pull request #233 from AeneasVerif/son/borrow-check

Add a `-borrow-check` option

1 files changed, 28 insertions, 0 deletions

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
+    }
+}