Skip to content

Commit a3f689e

Browse files
committed
Auto merge of #2922 - Vanille-N:tb-tests, r=RalfJung
TB: `box_exclusive_violation1` moved to `both_borrows` `box_noalias_violation` was already shared, it makes sense to test `box_exclusive_violation` with TB too.
2 parents 538479b + 8404d37 commit a3f689e

File tree

3 files changed

+48
-1
lines changed

3 files changed

+48
-1
lines changed

tests/fail/stacked_borrows/box_exclusive_violation1.rs renamed to tests/fail/both_borrows/box_exclusive_violation1.rs

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
//@revisions: stack tree
2+
//@[tree]compile-flags: -Zmiri-tree-borrows
3+
14
fn demo_box_advanced_unique(mut our: Box<i32>) -> i32 {
25
unknown_code_1(&*our);
36

@@ -24,7 +27,9 @@ fn unknown_code_1(x: &i32) {
2427

2528
fn unknown_code_2() {
2629
unsafe {
27-
*LEAK = 7; //~ ERROR: /write access .* tag does not exist in the borrow stack/
30+
*LEAK = 7;
31+
//~[stack]^ ERROR: /write access .* tag does not exist in the borrow stack/
32+
//~[tree]| ERROR: /write access through .* is forbidden/
2833
}
2934
}
3035

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
error: Undefined Behavior: write access through <TAG> is forbidden
2+
--> $DIR/box_exclusive_violation1.rs:LL:CC
3+
|
4+
LL | *LEAK = 7;
5+
| ^^^^^^^^^ write access through <TAG> is forbidden
6+
|
7+
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
8+
= help: the accessed tag <TAG> is a child of the conflicting tag <TAG>
9+
= help: the conflicting tag <TAG> has state Disabled which forbids this child write access
10+
help: the accessed tag <TAG> was created here
11+
--> $DIR/box_exclusive_violation1.rs:LL:CC
12+
|
13+
LL | fn unknown_code_1(x: &i32) {
14+
| ^
15+
help: the conflicting tag <TAG> was created here, in the initial state Frozen
16+
--> $DIR/box_exclusive_violation1.rs:LL:CC
17+
|
18+
LL | unknown_code_1(&*our);
19+
| ^^^^^
20+
help: the conflicting tag <TAG> later transitioned to Disabled due to a foreign write access at offsets [0x0..0x4]
21+
--> $DIR/box_exclusive_violation1.rs:LL:CC
22+
|
23+
LL | *our = 5;
24+
| ^^^^^^^^
25+
= help: this transition corresponds to a loss of read permissions
26+
= note: BACKTRACE (of the first span):
27+
= note: inside `unknown_code_2` at $DIR/box_exclusive_violation1.rs:LL:CC
28+
note: inside `demo_box_advanced_unique`
29+
--> $DIR/box_exclusive_violation1.rs:LL:CC
30+
|
31+
LL | unknown_code_2();
32+
| ^^^^^^^^^^^^^^^^
33+
note: inside `main`
34+
--> $DIR/box_exclusive_violation1.rs:LL:CC
35+
|
36+
LL | demo_box_advanced_unique(Box::new(0));
37+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
38+
39+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
40+
41+
error: aborting due to previous error
42+

0 commit comments

Comments
 (0)