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

Negative coverage: prove_place_is_movable / copy / premise prove_ty_is_copy(env, assumptions, state, &place.ty) => state

Premise at line 1078. Observed failure causes: failed_judgment.

copy
LineCoverageSource
10783(prove_ty_is_copy(env, assumptions, state, &place.ty) => state)
──────── ("copy")
108017(prove_place_is_movable(env, assumptions, state, place) => state)

3 tests failed proving this premise:


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

fn foo() -> Datum {
    exists<'r0, 'r1> {
        let x: Datum = Datum { value: 0_u32 };
        let r: &'r0 Datum = &'r1 x;
        let y: Datum = *r;
        return y;
    }
}
Failed proof tree
… (200 of 1420 nodes shown)

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

fn foo() -> Datum {
    exists<'r0, 'r1> {
        let x: Datum = Datum { value: 0_u32 };
        let r: &'r0 mut Datum = &'r1 mut x;
        let y: Datum = *r;
        return y;
    }
}
Failed proof tree
… (200 of 1420 nodes shown)

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

fn foo(f: Pair) -> () {
    let s: Datum = f.x;
}
Failed proof tree
… (200 of 332 nodes shown)

How to read this page