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_kind_for_place_use / copy

copy
LineCoverageSource
1009✗(prove_ty_is_copy(env, assumptions, state, &place.ty) => state)
──────── ("copy")
10113(access_kind_for_place_use(_env, _assumptions, state, _place) => (AccessKind::Read, state))

3 tests exercised this rule:

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

fn foo() -> u32 {
    let a: u32 = 0_u32;
    a;
    a;
    return 0_u32;
}
Proof tree
… (200 of 3433 nodes shown)

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:1132 (all coverage from this test)

fn main() -> () {
    let p: Pair = Pair { a: 2_u32, b: 3_u32 };
    p.b *= p.a + 4_u32;
    println!(p.b);
    println!(p.a);
}
Proof tree
… (200 of 3507 nodes shown)

How to read this page