summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2024-06-05 16:48:22 +0200
committerSon Ho2024-06-05 16:48:22 +0200
commit31c749247b30c1f88c0842a26f4f9956c92404be (patch)
tree3451722bea531e1a928e0f10ddf525f6fde4ee2f
parentc6ba96bf0723fd46432d73e52eaf6b0859c75fa8 (diff)
Add more tests
-rw-r--r--tests/src/loops-borrow-check-fail.borrow-check.out17
-rw-r--r--tests/src/loops-borrow-check-fail.rs21
-rw-r--r--tests/src/loops-borrow-check-negative.borrow-check.out3
-rw-r--r--tests/src/loops-borrow-check-negative.rs28
-rw-r--r--tests/src/loops-borrow-check.rs10
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;
+ }
+}