Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Positive coverage: access_permitted_by_loan / read-shared is ok

read-shared is ok
LineCoverageSource
──────── ("read-shared is ok")
9282(access_permitted_by_loan(
_env,
_assumptions,
state,
Loan { kind: RefKind::Shared, .. },
Access { kind: AccessKind::Read, .. },
_live_places,
) => state)

2 tests exercised this rule:


Source location: tests/borrowck.rs:5004 (all coverage from this test)

fn foo() -> u32 {
    exists<'l0> {
        let a: u32 = 0_u32;
        let p: &'l0 u32 = &'l0 a;
        let q: &'l0 u32 = p;
        let r: &'l0 u32 = p;
        p;
        return 0_u32;
    }
}
Proof tree
… (200 of 3585 nodes shown)

Source location: tests/codegen.rs:501 (all coverage from this test)

fn main() -> () {
    let x: i32 = 42_i32;
    exists<'a> {
        let r1: & 'a i32 = & 'a x;
        let r2: & 'a i32 = & 'a *r1;
        println!(*r2);
    }
}
Proof tree
… (200 of 3916 nodes shown)

How to read this page