summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon Ho2024-06-05 17:04:05 +0200
committerSon Ho2024-06-05 17:04:05 +0200
commitafe15cc3208b16b95109f056656c1c3d312841cc (patch)
treeae0dc5101d49e812366b3fb9ddb681f03dba486f /tests
parent7cb0914c68a055a308539ccc781fea8f30ef27bb (diff)
Add some negative tests for the borrow checker
Diffstat (limited to 'tests')
-rw-r--r--tests/src/borrow-check-negative.borrow-check.out15
-rw-r--r--tests/src/borrow-check-negative.rs90
2 files changed, 105 insertions, 0 deletions
diff --git a/tests/src/borrow-check-negative.borrow-check.out b/tests/src/borrow-check-negative.borrow-check.out
new file mode 100644
index 00000000..dc9dd5a7
--- /dev/null
+++ b/tests/src/borrow-check-negative.borrow-check.out
@@ -0,0 +1,15 @@
+[Info ] Imported: tests/llbc/borrow_check_negative.llbc
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 17:4-24:1
+[Error] Can't end abstraction 8 as it is set as non-endable
+Source: 'tests/src/borrow-check-negative.rs', lines 26:0-26:76
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 37:4-41:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 47:4-50:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 60:4-64:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 71:4-79:1
+[Error] Can not apply a projection to the ⊥ value
+Source: 'tests/src/borrow-check-negative.rs', lines 87:4-90:1
diff --git a/tests/src/borrow-check-negative.rs b/tests/src/borrow-check-negative.rs
new file mode 100644
index 00000000..697546dd
--- /dev/null
+++ b/tests/src/borrow-check-negative.rs
@@ -0,0 +1,90 @@
+//@ [!borrow-check] skip
+//@ [borrow-check] known-failure
+// Some negative tests for borrow checking
+
+// This succeeds
+fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T {
+ if b {
+ x
+ } else {
+ y
+ }
+}
+
+pub fn choose_test() {
+ let mut x = 0;
+ let mut y = 0;
+ let z = choose(true, &mut x, &mut y);
+ *z += 1;
+ assert!(*z == 1);
+ // drop(z)
+ assert!(x == 1);
+ assert!(y == 0);
+ assert!(*z == 1); // z is not valid anymore
+}
+
+fn choose_wrong<'a, 'b, T>(b: bool, x: &'a mut T, y: &'b mut T) -> &'a mut T {
+ if b {
+ x
+ } else {
+ y // Expected lifetime 'a
+ }
+}
+
+fn test_mut1(b: bool) {
+ let mut x = 0;
+ let mut y = 1;
+ let z = if b { &mut x } else { &mut y };
+ *z += 1;
+ assert!(x >= 0);
+ *z += 1; // z is not valid anymore
+}
+
+#[allow(unused_assignments)]
+fn test_mut2(b: bool) {
+ let mut x = 0;
+ let mut y = 1;
+ let z = if b { &x } else { &y };
+ x += 1;
+ assert!(*z == 0); // z is not valid anymore
+}
+
+fn test_move1<T>(x: T) -> T {
+ let _ = x;
+ return x; // x has been moved
+}
+
+pub fn refs_test1() {
+ let mut x = 0;
+ let mut px = &mut x;
+ let ppx = &mut px;
+ **ppx = 1;
+ assert!(x == 1);
+ assert!(**ppx == 1); // ppx has ended
+}
+
+pub fn refs_test2() {
+ let mut x = 0;
+ let mut y = 1;
+ let mut px = &mut x;
+ let py = &mut y;
+ let ppx = &mut px;
+ *ppx = py;
+ **ppx = 2;
+ assert!(*px == 2);
+ assert!(x == 0);
+ assert!(*py == 2);
+ assert!(y == 2);
+ assert!(**ppx == 2); // ppx has ended
+}
+
+pub fn test_box1() {
+ use std::ops::Deref;
+ use std::ops::DerefMut;
+ let mut b: Box<i32> = Box::new(0);
+ let x0 = b.deref_mut();
+ *x0 = 1;
+ let x1 = b.deref();
+ assert!(*x1 == 1);
+ assert!(*x0 == 1); // x0 has ended
+}