box_exclusive_violation

3 files changed, 48 insertions, 1 deletions

diff --git a/src/tools/miri/tests/fail/stacked_borrows/box_exclusive_violation1.rs b/src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.rs
index 87a6b7bbd67..4936c1a9018 100644
--- a/src/tools/miri/tests/fail/stacked_borrows/box_exclusive_violation1.rs
+++ b/src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.rs
@@ -1,3 +1,6 @@
+//@revisions: stack tree
+//@[tree]compile-flags: -Zmiri-tree-borrows
+
 fn demo_box_advanced_unique(mut our: Box<i32>) -> i32 {
     unknown_code_1(&*our);
 
@@ -24,7 +27,9 @@ fn unknown_code_1(x: &i32) {
 
 fn unknown_code_2() {
     unsafe {
-        *LEAK = 7; //~ ERROR: /write access .* tag does not exist in the borrow stack/
+        *LEAK = 7;
+        //~[stack]^ ERROR: /write access .* tag does not exist in the borrow stack/
+        //~[tree]| ERROR: /write access through .* is forbidden/
     }
 }
 
diff --git a/src/tools/miri/tests/fail/stacked_borrows/box_exclusive_violation1.stderr b/src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.stack.stderr
index 76f4e81f71b..76f4e81f71b 100644
--- a/src/tools/miri/tests/fail/stacked_borrows/box_exclusive_violation1.stderr
+++ b/src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.stack.stderr
diff --git a/src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.tree.stderr b/src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.tree.stderr
new file mode 100644
index 00000000000..97f82db6fe7
--- /dev/null
+++ b/src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.tree.stderr
@@ -0,0 +1,42 @@
+error: Undefined Behavior: write access through <TAG> is forbidden
+  --> $DIR/box_exclusive_violation1.rs:LL:CC
+   |
+LL |         *LEAK = 7;
+   |         ^^^^^^^^^ write access through <TAG> is forbidden
+   |
+   = help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
+   = help: the accessed tag <TAG> is a child of the conflicting tag <TAG>
+   = help: the conflicting tag <TAG> has state Disabled which forbids this child write access
+help: the accessed tag <TAG> was created here
+  --> $DIR/box_exclusive_violation1.rs:LL:CC
+   |
+LL | fn unknown_code_1(x: &i32) {
+   |                   ^
+help: the conflicting tag <TAG> was created here, in the initial state Frozen
+  --> $DIR/box_exclusive_violation1.rs:LL:CC
+   |
+LL |     unknown_code_1(&*our);
+   |                    ^^^^^
+help: the conflicting tag <TAG> later transitioned to Disabled due to a foreign write access at offsets [0x0..0x4]
+  --> $DIR/box_exclusive_violation1.rs:LL:CC
+   |
+LL |     *our = 5;
+   |     ^^^^^^^^
+   = help: this transition corresponds to a loss of read permissions
+   = note: BACKTRACE (of the first span):
+   = note: inside `unknown_code_2` at $DIR/box_exclusive_violation1.rs:LL:CC
+note: inside `demo_box_advanced_unique`
+  --> $DIR/box_exclusive_violation1.rs:LL:CC
+   |
+LL |     unknown_code_2();
+   |     ^^^^^^^^^^^^^^^^
+note: inside `main`
+  --> $DIR/box_exclusive_violation1.rs:LL:CC
+   |
+LL |     demo_box_advanced_unique(Box::new(0));
+   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+