diff options
author | Son Ho | 2024-06-05 17:04:05 +0200 |
---|---|---|
committer | Son Ho | 2024-06-05 17:04:05 +0200 |
commit | afe15cc3208b16b95109f056656c1c3d312841cc (patch) | |
tree | ae0dc5101d49e812366b3fb9ddb681f03dba486f /tests/src | |
parent | 7cb0914c68a055a308539ccc781fea8f30ef27bb (diff) |
Add some negative tests for the borrow checker
Diffstat (limited to '')
-rw-r--r-- | tests/src/borrow-check-negative.borrow-check.out | 15 | ||||
-rw-r--r-- | tests/src/borrow-check-negative.rs | 90 |
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 @@ +[[92mInfo[39m ] Imported: tests/llbc/borrow_check_negative.llbc +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 17:4-24:1 +[[91mError[39m] Can't end abstraction 8 as it is set as non-endable +Source: 'tests/src/borrow-check-negative.rs', lines 26:0-26:76 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 37:4-41:1 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 47:4-50:1 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 60:4-64:1 +[[91mError[39m] Can not apply a projection to the ⊥ value +Source: 'tests/src/borrow-check-negative.rs', lines 71:4-79:1 +[[91mError[39m] 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 +} |