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

Add a `-borrow-check` option

1 files changed, 21 insertions, 0 deletions

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