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: borrow_check_expr / place / premise access_permitted(env, assumptions, state, Access::new(access_kind, place), places_live_on_exit) => state

Premise at line 504. Observed failure causes: failed_judgment.

place
LineCoverageSource
5022(borrow_check_place_expr(env, assumptions, state, place) => (place, state))
503✗(access_kind_for_place_use(env, assumptions, state, place) => (access_kind, state))
50413(access_permitted(env, assumptions, state, Access::new(access_kind, place), places_live_on_exit) => state)
505N/A(let state = if matches!(access_kind, AccessKind::Move) { state.with_uninit(&place.to_place_expression()) } else { state.clone() })
5063(prove_place_is_movable(env, assumptions, state, place) => state)
──────── ("place")
50871(borrow_check_expr(env, assumptions, state, Expr::Place(place), places_live_on_exit) => (&place.ty, state))

13 tests failed proving this premise:

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

fn foo() -> u32 {
    let x: u32;
    return x;
}
Failed proof tree

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

fn foo() -> Datum {
    let x: Datum = Datum { value: 0_u32 };
    let y: Datum = x;
    let z: Datum = x;
    return z;
}
Failed proof tree

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

fn foo() -> u32 {
    let x: u32;
    if true {
        x = 1_u32;
    } else {
    }
    return x;
}
Failed proof tree

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

fn foo() -> u32 {
    let x: u32;
    if true {
        x = 1_u32;
    }
    return x;
}
Failed proof tree

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

fn foo() -> Datum {
    let x: Datum = Datum { value: 0_u32 };
    if true {
        let y: Datum = x;
    }
    let z: Datum = x;
    return z;
}
Failed proof tree

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

fn foo() -> u32 {
    let x: Pair = Pair {
        first: Datum { value: 1_u32 },
        second: Datum { value: 2_u32 },
    };
    let a: Datum = x.first;
    let b: Pair = x;
    return 0_u32;
}
Failed proof tree

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

fn foo() -> Datum {
    let x: Pair = Pair {
        first: Datum { value: 1_u32 },
        second: Datum { value: 2_u32 },
    };
    let a: Datum = x.first;
    let b: Datum = x.first;
    return b;
}
Failed proof tree

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

fn foo() -> Datum {
    let x: Pair = Pair {
        first: Datum { value: 1_u32 },
        second: Datum { value: 2_u32 },
    };
    let a: Pair = x;
    let b: Datum = x.first;
    return b;
}
Failed proof tree

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

fn foo() -> u32 {
    let x: Outer = Outer {
        foo: Inner { bar: 1_u32 },
    };
    let a: Inner = x.foo;
    let b: u32 = x.foo.bar;
    return b;
}
Failed proof tree

Source location: tests/borrowck.rs:1957 (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 = x;
        return *r;
    }
}
Failed proof tree

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

fn foo() -> u32 {
    let x: u32;
    return x;
}

Proof trees omitted for the remaining 3 tests; each one is on its test’s page in Coverage by test.

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

fn foo() -> i32 {
    exists<'r0, 'r1> {
        let x: i32 = 0_i32;
        let r: &'r0 i32;
        'a: loop {
            r; // this *may* read from `y` in a previous iteration
            let y: i32 = 0_i32;
            r = &'r1 y;
            continue 'a;
        }
    }
}

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

fn foo() -> u32 {
    exists<'r0, 'r1> {
        let v1: u32 = 22_u32;
        let v2: &'r0 mut u32 = &'r1 mut v1;
        let w: Wrapper = Wrapper { value: v1 };
        return *v2;
    }
}