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: prove_place_is_movable / field

field
LineCoverageSource
872(prove_place_is_movable(env, assumptions, state, prefix) => state)
──────── ("field")
8743(prove_place_is_movable(
env,
assumptions,
state,
TypedPlaceExpressionData::Field(prefix, _),
) => state)

3 tests exercised this rule:


Source location: tests/borrowck.rs:253

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.second;
    return b;
}
Proof tree
… (200 of 1154 nodes shown)

Source location: tests/codegen.rs:141

fn main() -> () {
    let p: Pair = Pair { x: 10 _ i32, y: 20 _ i32 };
    println!(p.x);
    println!(p.y);
}
Proof tree
… (200 of 1068 nodes shown)

Source location: tests/codegen.rs:264

fn main() -> () {
    let w: Wrapper<i32> = Wrapper::<i32> { val: 42 _ i32 };
    println!(w.val);
}
Proof tree
… (200 of 1048 nodes shown)