From 7566ed8ff4db1549feeaebe0ed1ca2e0de2c9c01 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 28 Apr 2023 12:58:19 +0200 Subject: [PATCH] tweak wording --- .../tree_borrows/diagnostics.rs | 67 +++++++++---------- src/tools/miri/src/diagnostics.rs | 15 ++--- .../tree-borrows/alternate-read-write.stderr | 20 +++--- .../fail/tree-borrows/error-range.stderr | 24 +++---- .../tree-borrows/fragile-data-race.stderr | 16 ++--- .../fail/tree-borrows/outside-range.stderr | 13 ++-- .../fail/tree-borrows/read-to-local.stderr | 16 ++--- .../reserved/cell-protected-write.stderr | 13 ++-- .../reserved/int-protected-write.stderr | 13 ++-- .../tree-borrows/strongly-protected.stderr | 12 ++-- .../tree-borrows/write-during-2phase.stderr | 12 ++-- 11 files changed, 111 insertions(+), 110 deletions(-) diff --git a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs index 18d540dfd1a69..2c6d27ced0180 100644 --- a/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs +++ b/src/tools/miri/src/borrow_tracker/tree_borrows/diagnostics.rs @@ -70,7 +70,7 @@ impl HistoryData { let this = format!("the {tag_name} tag {tag:?}"); let msg_initial_state = format!(", in the initial state {}", created.1); let msg_creation = format!( - "{this} was created here{maybe_msg_initial_state}.", + "{this} was created here{maybe_msg_initial_state}", maybe_msg_initial_state = if show_initial_state { &msg_initial_state } else { "" }, ); @@ -79,8 +79,8 @@ impl HistoryData { { // NOTE: `offset` is explicitly absent from the error message, it has no significance // to the user. The meaningful one is `access_range`. - self.events.push((Some(span.data()), format!("{this} then transitioned {transition} due to a {rel} {access_kind} at offsets {access_range:?}.", rel = if is_foreign { "foreign" } else { "child" }))); - self.events.push((None, format!("this corresponds to {}.", transition.summary()))); + self.events.push((Some(span.data()), format!("{this} then transitioned {transition} due to a {rel} {access_kind} at offsets {access_range:?}", rel = if is_foreign { "foreign" } else { "child" }))); + self.events.push((None, format!("this corresponds to {}", transition.summary()))); } } } @@ -266,50 +266,49 @@ impl TbError<'_> { let accessed = self.accessed_info; let conflicting = self.conflicting_info; let accessed_is_conflicting = accessed.tag == conflicting.tag; - let (pre_error, title, relation, problem, conflicting_tag_name) = match self.error_kind { + let (pre_error, title, details, conflicting_tag_name) = match self.error_kind { ChildAccessForbidden(perm) => { let conflicting_tag_name = if accessed_is_conflicting { "accessed" } else { "conflicting" }; - ( - perm, - format!("{kind} through {accessed} is forbidden."), - (!accessed_is_conflicting).then_some(format!( - "the accessed tag {accessed} is a child of the conflicting tag {conflicting}." - )), - format!( - "the {conflicting_tag_name} tag {conflicting} has state {perm} which forbids child {kind}es." - ), - conflicting_tag_name, - ) + let title = format!("{kind} through {accessed} is forbidden"); + let mut details = Vec::new(); + if !accessed_is_conflicting { + details.push(format!( + "the accessed tag {accessed} is a child of the conflicting tag {conflicting}" + )); + } + details.push(format!( + "the {conflicting_tag_name} tag {conflicting} has state {perm} which forbids child {kind}es" + )); + (perm, title, details, conflicting_tag_name) } ProtectedTransition(transition) => { let conflicting_tag_name = "protected"; - ( - transition.started(), - format!("{kind} through {accessed} is forbidden."), - Some(format!( - "the accessed tag {accessed} is a foreign tag for the {conflicting_tag_name} tag {conflicting}." - )), + let title = format!("{kind} through {accessed} is forbidden"); + let details = vec![ + format!( + "the accessed tag {accessed} is foreign to the {conflicting_tag_name} tag {conflicting} (i.e., it is not a child)" + ), + format!( + "the access would cause the {conflicting_tag_name} tag {conflicting} to transition {transition}" + ), format!( - "the access would cause the {conflicting_tag_name} tag {conflicting} to transition {transition}. This is {loss}, which is not allowed for protected tags.", + "this is {loss}, which is not allowed for protected tags", loss = transition.summary(), ), - conflicting_tag_name, - ) + ]; + (transition.started(), title, details, conflicting_tag_name) } ProtectedDealloc => { let conflicting_tag_name = "strongly protected"; - ( - started_as, - format!("deallocation through {accessed} is forbidden."), - Some(format!( - "the allocation of the accessed tag {accessed} also contains the {conflicting_tag_name} tag {conflicting}." - )), + let title = format!("deallocation through {accessed} is forbidden"); + let details = vec![ format!( - "the {conflicting_tag_name} tag {conflicting} disallows deallocations." + "the allocation of the accessed tag {accessed} also contains the {conflicting_tag_name} tag {conflicting}" ), - conflicting_tag_name, - ) + format!("the {conflicting_tag_name} tag {conflicting} disallows deallocations"), + ]; + (started_as, title, details, conflicting_tag_name) } }; let pre_transition = PermTransition::from(started_as, pre_error).unwrap(); @@ -322,7 +321,7 @@ impl TbError<'_> { conflicting_tag_name, true, ); - err_machine_stop!(TerminationInfo::TreeBorrowsUb { title, relation, problem, history }) + err_machine_stop!(TerminationInfo::TreeBorrowsUb { title, details, history }) } } diff --git a/src/tools/miri/src/diagnostics.rs b/src/tools/miri/src/diagnostics.rs index b4bf93a73d989..aeba0ea5a9524 100644 --- a/src/tools/miri/src/diagnostics.rs +++ b/src/tools/miri/src/diagnostics.rs @@ -25,8 +25,7 @@ pub enum TerminationInfo { }, TreeBorrowsUb { title: String, - relation: Option, - problem: String, + details: Vec, history: tree_diagnostics::HistoryData, }, Int2PtrWithStrictProvenance, @@ -222,13 +221,13 @@ pub fn report_error<'tcx, 'mir>( } helps }, - TreeBorrowsUb { title: _, relation, problem, history } => { - let mut helps = Vec::new(); - if let Some(relation) = relation { - helps.push((None, relation.clone())); + TreeBorrowsUb { title: _, details, history } => { + let mut helps = vec![ + (None, format!("this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental")) + ]; + for m in details { + helps.push((None, m.clone())); } - helps.push((None, problem.clone())); - helps.push((None, format!("this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental"))); for event in history.events.clone() { helps.push(event); } diff --git a/src/tools/miri/tests/fail/tree-borrows/alternate-read-write.stderr b/src/tools/miri/tests/fail/tree-borrows/alternate-read-write.stderr index 1c9fe57bfb381..bb601fc88352d 100644 --- a/src/tools/miri/tests/fail/tree-borrows/alternate-read-write.stderr +++ b/src/tools/miri/tests/fail/tree-borrows/alternate-read-write.stderr @@ -1,34 +1,34 @@ -error: Undefined Behavior: write access through is forbidden. +error: Undefined Behavior: write access through is forbidden --> $DIR/alternate-read-write.rs:LL:CC | LL | *y += 1; // Failure - | ^^^^^^^ write access through is forbidden. + | ^^^^^^^ write access through is forbidden | - = help: the accessed tag is a child of the conflicting tag . - = help: the conflicting tag has state Frozen which forbids child write accesses. = 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 was created here. + = help: the accessed tag is a child of the conflicting tag + = help: the conflicting tag has state Frozen which forbids child write accesses +help: the accessed tag was created here --> $DIR/alternate-read-write.rs:LL:CC | LL | let y = unsafe { &mut *(x as *mut u8) }; | ^^^^^^^^^^^^^^^^^^^^ -help: the conflicting tag was created here, in the initial state Reserved. +help: the conflicting tag was created here, in the initial state Reserved --> $DIR/alternate-read-write.rs:LL:CC | LL | let y = unsafe { &mut *(x as *mut u8) }; | ^^^^^^^^^^^^^^^^^^^^ -help: the conflicting tag then transitioned from Reserved to Active due to a child write access at offsets [0x0..0x1]. +help: the conflicting tag then transitioned from Reserved to Active due to a child write access at offsets [0x0..0x1] --> $DIR/alternate-read-write.rs:LL:CC | LL | *y += 1; // Success | ^^^^^^^ - = help: this corresponds to an activation. -help: the conflicting tag then transitioned from Active to Frozen due to a foreign read access at offsets [0x0..0x1]. + = help: this corresponds to an activation +help: the conflicting tag then transitioned from Active to Frozen due to a foreign read access at offsets [0x0..0x1] --> $DIR/alternate-read-write.rs:LL:CC | LL | let _val = *x; | ^^ - = help: this corresponds to a loss of write permissions. + = help: this corresponds to a loss of write permissions = note: BACKTRACE (of the first span): = note: inside `main` at $DIR/alternate-read-write.rs:LL:CC diff --git a/src/tools/miri/tests/fail/tree-borrows/error-range.stderr b/src/tools/miri/tests/fail/tree-borrows/error-range.stderr index 870beeda04df6..bc829fd86d350 100644 --- a/src/tools/miri/tests/fail/tree-borrows/error-range.stderr +++ b/src/tools/miri/tests/fail/tree-borrows/error-range.stderr @@ -1,40 +1,40 @@ -error: Undefined Behavior: read access through is forbidden. +error: Undefined Behavior: read access through is forbidden --> $DIR/error-range.rs:LL:CC | LL | rmut[5] += 1; - | ^^^^^^^^^^^^ read access through is forbidden. + | ^^^^^^^^^^^^ read access through is forbidden | - = help: the accessed tag is a child of the conflicting tag . - = help: the conflicting tag has state Disabled which forbids child read accesses. = 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 was created here. + = help: the accessed tag is a child of the conflicting tag + = help: the conflicting tag has state Disabled which forbids child read accesses +help: the accessed tag was created here --> $DIR/error-range.rs:LL:CC | LL | let rmut = &mut *addr_of_mut!(data[0..6]); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -help: the conflicting tag was created here, in the initial state Reserved. +help: the conflicting tag was created here, in the initial state Reserved --> $DIR/error-range.rs:LL:CC | LL | let rmut = &mut *addr_of_mut!(data[0..6]); | ^^^^ -help: the conflicting tag then transitioned from Reserved to Active due to a child write access at offsets [0x5..0x6]. +help: the conflicting tag then transitioned from Reserved to Active due to a child write access at offsets [0x5..0x6] --> $DIR/error-range.rs:LL:CC | LL | rmut[5] += 1; | ^^^^^^^^^^^^ - = help: this corresponds to an activation. -help: the conflicting tag then transitioned from Active to Frozen due to a foreign read access at offsets [0x5..0x6]. + = help: this corresponds to an activation +help: the conflicting tag then transitioned from Active to Frozen due to a foreign read access at offsets [0x5..0x6] --> $DIR/error-range.rs:LL:CC | LL | let _v = data[5]; | ^^^^^^^ - = help: this corresponds to a loss of write permissions. -help: the conflicting tag then transitioned from Frozen to Disabled due to a foreign write access at offsets [0x5..0x6]. + = help: this corresponds to a loss of write permissions +help: the conflicting tag then transitioned from Frozen to Disabled due to a foreign write access at offsets [0x5..0x6] --> $DIR/error-range.rs:LL:CC | LL | data[5] = 1; | ^^^^^^^^^^^ - = help: this corresponds to a loss of read permissions. + = help: this corresponds to a loss of read permissions = note: BACKTRACE (of the first span): = note: inside `main` at $DIR/error-range.rs:LL:CC diff --git a/src/tools/miri/tests/fail/tree-borrows/fragile-data-race.stderr b/src/tools/miri/tests/fail/tree-borrows/fragile-data-race.stderr index 9ef4b10a1bf35..8e80bdd63c0be 100644 --- a/src/tools/miri/tests/fail/tree-borrows/fragile-data-race.stderr +++ b/src/tools/miri/tests/fail/tree-borrows/fragile-data-race.stderr @@ -1,28 +1,28 @@ -error: Undefined Behavior: write access through is forbidden. +error: Undefined Behavior: write access through is forbidden --> $DIR/fragile-data-race.rs:LL:CC | LL | unsafe { *p = 1 }; - | ^^^^^^ write access through is forbidden. + | ^^^^^^ write access through is forbidden | - = help: the accessed tag is a child of the conflicting tag . - = help: the conflicting tag has state Frozen which forbids child write accesses. = 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 was created here. + = help: the accessed tag is a child of the conflicting tag + = help: the conflicting tag has state Frozen which forbids child write accesses +help: the accessed tag was created here --> $DIR/fragile-data-race.rs:LL:CC | LL | fn thread_1(x: &mut u8) -> SendPtr { | ^ -help: the conflicting tag was created here, in the initial state Reserved. +help: the conflicting tag was created here, in the initial state Reserved --> RUSTLIB/std/src/panic.rs:LL:CC | LL | pub fn catch_unwind R + UnwindSafe, R>(f: F) -> Result { | ^ -help: the conflicting tag then transitioned from Reserved to Frozen due to a foreign read access at offsets [0x0..0x1]. +help: the conflicting tag then transitioned from Reserved to Frozen due to a foreign read access at offsets [0x0..0x1] --> RUSTLIB/core/src/ptr/mod.rs:LL:CC | LL | crate::intrinsics::read_via_copy(src) | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - = help: this corresponds to a loss of write permissions. + = help: this corresponds to a loss of write permissions = note: BACKTRACE (of the first span): = note: inside `main` at $DIR/fragile-data-race.rs:LL:CC diff --git a/src/tools/miri/tests/fail/tree-borrows/outside-range.stderr b/src/tools/miri/tests/fail/tree-borrows/outside-range.stderr index 5e76a3f2c0dda..14696c704fc1b 100644 --- a/src/tools/miri/tests/fail/tree-borrows/outside-range.stderr +++ b/src/tools/miri/tests/fail/tree-borrows/outside-range.stderr @@ -1,18 +1,19 @@ -error: Undefined Behavior: write access through is forbidden. +error: Undefined Behavior: write access through is forbidden --> $DIR/outside-range.rs:LL:CC | LL | *y.add(3) = 42; - | ^^^^^^^^^^^^^^ write access through is forbidden. + | ^^^^^^^^^^^^^^ write access through is forbidden | - = help: the accessed tag is a foreign tag for the protected tag . - = help: the access would cause the protected tag to transition from Reserved to Disabled. This is a loss of read and write permissions, which is not allowed for protected tags. = 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 was created here. + = help: the accessed tag is foreign to the protected tag (i.e., it is not a child) + = help: the access would cause the protected tag to transition from Reserved to Disabled + = help: this is a loss of read and write permissions, which is not allowed for protected tags +help: the accessed tag was created here --> $DIR/outside-range.rs:LL:CC | LL | let raw = data.as_mut_ptr(); | ^^^^^^^^^^^^^^^^^ -help: the protected tag was created here, in the initial state Reserved. +help: the protected tag was created here, in the initial state Reserved --> $DIR/outside-range.rs:LL:CC | LL | unsafe fn stuff(x: &mut u8, y: *mut u8) { diff --git a/src/tools/miri/tests/fail/tree-borrows/read-to-local.stderr b/src/tools/miri/tests/fail/tree-borrows/read-to-local.stderr index 4486f7a5a6fe6..8c9c2f8f9656b 100644 --- a/src/tools/miri/tests/fail/tree-borrows/read-to-local.stderr +++ b/src/tools/miri/tests/fail/tree-borrows/read-to-local.stderr @@ -1,28 +1,28 @@ -error: Undefined Behavior: write access through is forbidden. +error: Undefined Behavior: write access through is forbidden --> $DIR/read-to-local.rs:LL:CC | LL | *ptr = 0; - | ^^^^^^^^ write access through is forbidden. + | ^^^^^^^^ write access through is forbidden | - = help: the accessed tag has state Frozen which forbids child write accesses. = 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 was created here, in the initial state Reserved. + = help: the accessed tag has state Frozen which forbids child write accesses +help: the accessed tag was created here, in the initial state Reserved --> $DIR/read-to-local.rs:LL:CC | LL | let mref = &mut root; | ^^^^^^^^^ -help: the accessed tag then transitioned from Reserved to Active due to a child write access at offsets [0x0..0x1]. +help: the accessed tag then transitioned from Reserved to Active due to a child write access at offsets [0x0..0x1] --> $DIR/read-to-local.rs:LL:CC | LL | *ptr = 0; // Write | ^^^^^^^^ - = help: this corresponds to an activation. -help: the accessed tag then transitioned from Active to Frozen due to a foreign read access at offsets [0x0..0x1]. + = help: this corresponds to an activation +help: the accessed tag then transitioned from Active to Frozen due to a foreign read access at offsets [0x0..0x1] --> $DIR/read-to-local.rs:LL:CC | LL | assert_eq!(root, 0); // Parent Read | ^^^^^^^^^^^^^^^^^^^ - = help: this corresponds to a loss of write permissions. + = help: this corresponds to a loss of write permissions = note: BACKTRACE (of the first span): = note: inside `main` at $DIR/read-to-local.rs:LL:CC = note: this error originates in the macro `assert_eq` (in Nightly builds, run with -Z macro-backtrace for more info) diff --git a/src/tools/miri/tests/fail/tree-borrows/reserved/cell-protected-write.stderr b/src/tools/miri/tests/fail/tree-borrows/reserved/cell-protected-write.stderr index efeea52b72253..b85793ff06337 100644 --- a/src/tools/miri/tests/fail/tree-borrows/reserved/cell-protected-write.stderr +++ b/src/tools/miri/tests/fail/tree-borrows/reserved/cell-protected-write.stderr @@ -8,21 +8,22 @@ Warning: this tree is indicative only. Some tags may have been hidden. | Re*| │ └──── Strongly protected | Re*| └──── ────────────────────────────────────────────────────────────────────── -error: Undefined Behavior: write access through (y, callee:y, caller:y) is forbidden. +error: Undefined Behavior: write access through (y, callee:y, caller:y) is forbidden --> $DIR/cell-protected-write.rs:LL:CC | LL | *y = 1; - | ^^^^^^ write access through (y, callee:y, caller:y) is forbidden. + | ^^^^^^ write access through (y, callee:y, caller:y) is forbidden | - = help: the accessed tag (y, callee:y, caller:y) is a foreign tag for the protected tag (callee:x). - = help: the access would cause the protected tag (callee:x) to transition from Reserved to Disabled. This is a loss of read and write permissions, which is not allowed for protected tags. = 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 was created here. + = help: the accessed tag (y, callee:y, caller:y) is foreign to the protected tag (callee:x) (i.e., it is not a child) + = help: the access would cause the protected tag (callee:x) to transition from Reserved to Disabled + = help: this is a loss of read and write permissions, which is not allowed for protected tags +help: the accessed tag was created here --> $DIR/cell-protected-write.rs:LL:CC | LL | let y = (&mut *n).get(); | ^^^^^^^^^ -help: the protected tag was created here, in the initial state Reserved. +help: the protected tag was created here, in the initial state Reserved --> $DIR/cell-protected-write.rs:LL:CC | LL | unsafe fn write_second(x: &mut UnsafeCell, y: *mut u8) { diff --git a/src/tools/miri/tests/fail/tree-borrows/reserved/int-protected-write.stderr b/src/tools/miri/tests/fail/tree-borrows/reserved/int-protected-write.stderr index 181577787651b..5de7dc0c7c51f 100644 --- a/src/tools/miri/tests/fail/tree-borrows/reserved/int-protected-write.stderr +++ b/src/tools/miri/tests/fail/tree-borrows/reserved/int-protected-write.stderr @@ -8,21 +8,22 @@ Warning: this tree is indicative only. Some tags may have been hidden. | Res| │ └──── Strongly protected | Res| └──── ────────────────────────────────────────────────────────────────────── -error: Undefined Behavior: write access through (y, callee:y, caller:y) is forbidden. +error: Undefined Behavior: write access through (y, callee:y, caller:y) is forbidden --> $DIR/int-protected-write.rs:LL:CC | LL | *y = 0; - | ^^^^^^ write access through (y, callee:y, caller:y) is forbidden. + | ^^^^^^ write access through (y, callee:y, caller:y) is forbidden | - = help: the accessed tag (y, callee:y, caller:y) is a foreign tag for the protected tag (callee:x). - = help: the access would cause the protected tag (callee:x) to transition from Reserved to Disabled. This is a loss of read and write permissions, which is not allowed for protected tags. = 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 was created here. + = help: the accessed tag (y, callee:y, caller:y) is foreign to the protected tag (callee:x) (i.e., it is not a child) + = help: the access would cause the protected tag (callee:x) to transition from Reserved to Disabled + = help: this is a loss of read and write permissions, which is not allowed for protected tags +help: the accessed tag was created here --> $DIR/int-protected-write.rs:LL:CC | LL | let y = (&mut *n) as *mut _; | ^^^^^^^^^ -help: the protected tag was created here, in the initial state Reserved. +help: the protected tag was created here, in the initial state Reserved --> $DIR/int-protected-write.rs:LL:CC | LL | unsafe fn write_second(x: &mut u8, y: *mut u8) { diff --git a/src/tools/miri/tests/fail/tree-borrows/strongly-protected.stderr b/src/tools/miri/tests/fail/tree-borrows/strongly-protected.stderr index 174951d6f00d4..97088d5854cc9 100644 --- a/src/tools/miri/tests/fail/tree-borrows/strongly-protected.stderr +++ b/src/tools/miri/tests/fail/tree-borrows/strongly-protected.stderr @@ -1,18 +1,18 @@ -error: Undefined Behavior: deallocation through is forbidden. +error: Undefined Behavior: deallocation through is forbidden --> RUSTLIB/alloc/src/alloc.rs:LL:CC | LL | unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) } - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ deallocation through is forbidden. + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ deallocation through is forbidden | - = help: the allocation of the accessed tag also contains the strongly protected tag . - = help: the strongly protected tag disallows deallocations. = 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 was created here. + = help: the allocation of the accessed tag also contains the strongly protected tag + = help: the strongly protected tag disallows deallocations +help: the accessed tag was created here --> $DIR/strongly-protected.rs:LL:CC | LL | drop(unsafe { Box::from_raw(raw) }); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -help: the strongly protected tag was created here, in the initial state Reserved. +help: the strongly protected tag was created here, in the initial state Reserved --> $DIR/strongly-protected.rs:LL:CC | LL | fn inner(x: &mut i32, f: fn(&mut i32)) { diff --git a/src/tools/miri/tests/fail/tree-borrows/write-during-2phase.stderr b/src/tools/miri/tests/fail/tree-borrows/write-during-2phase.stderr index b27d650d9f81d..f6285bdcf16d4 100644 --- a/src/tools/miri/tests/fail/tree-borrows/write-during-2phase.stderr +++ b/src/tools/miri/tests/fail/tree-borrows/write-during-2phase.stderr @@ -1,12 +1,12 @@ -error: Undefined Behavior: read access through is forbidden. +error: Undefined Behavior: read access through is forbidden --> $DIR/write-during-2phase.rs:LL:CC | LL | fn add(&mut self, n: u64) -> u64 { - | ^^^^^^^^^ read access through is forbidden. + | ^^^^^^^^^ read access through is forbidden | - = help: the accessed tag has state Disabled which forbids child read accesses. = 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 was created here, in the initial state Reserved. + = help: the accessed tag has state Disabled which forbids child read accesses +help: the accessed tag was created here, in the initial state Reserved --> $DIR/write-during-2phase.rs:LL:CC | LL | let _res = f.add(unsafe { @@ -18,12 +18,12 @@ LL | | *inner = 42; LL | | n LL | | }); | |______^ -help: the accessed tag then transitioned from Reserved to Disabled due to a foreign write access at offsets [0x0..0x8]. +help: the accessed tag then transitioned from Reserved to Disabled due to a foreign write access at offsets [0x0..0x8] --> $DIR/write-during-2phase.rs:LL:CC | LL | *inner = 42; | ^^^^^^^^^^^ - = help: this corresponds to a loss of read and write permissions. + = help: this corresponds to a loss of read and write permissions = note: BACKTRACE (of the first span): = note: inside `Foo::add` at $DIR/write-during-2phase.rs:LL:CC note: inside `main`