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: borrow_check_place_expr / struct field

struct field
LineCoverageSource
688✗(borrow_check_place_expr(env, assumptions, state, prefix) => (prefix_typed, state))
6891(prove_ty_is_rigid(env, assumptions, state, &prefix_typed.ty) => (RigidTy { name: RigidName::AdtId(adt_id), parameters }, state))
690✗(let Struct { id: _, binder } = env.crates().struct_named(&adt_id)?)
691✗(let StructBoundData { where_clauses, fields } = binder.instantiate_with(&parameters)?)
692✗(prove_where_clauses(env, assumptions, state, where_clauses) => state)
693✗(field in fields)
6941(if field.name == *field_name)
──────── ("struct field")
69619(borrow_check_place_expr(env, assumptions, state, PlaceExpr::Field { prefix, field_name }) => (
TypedPlaceExpr::new(&field.ty, TypedPlaceExpressionData::field(prefix_typed, field_name, adt_id, VariantId::for_struct())),
state,
))

19 tests exercised this rule:

Source location: tests/borrowck.rs:495 (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.second;
    return b;
}
Proof tree
… (200 of 3542 nodes shown)

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

fn min_problem_case_4<'a>(list: &'a mut Map, list2: &'a mut Map) -> u32 {
    exists<'r0> {
        let num: &'r0 mut u32 = &'r0 mut (*list).value;
        list = &'a mut *list2;
        num;
        return 0_u32;
    }
}
Proof tree
… (200 of 3676 nodes shown)

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

fn foo() -> u32 {
    exists<'r0, 'r1, 'r2, 'r3> {
        let p: Point = Point { x: 0_u32, y: 0_u32 };
        let b1: &'r0 mut u32 = &'r1 mut p.x;
        let b2: &'r2 mut u32 = &'r3 mut p.y;
        *b1 = 1_u32;
        *b2 = 2_u32;
        return 0_u32;
    }
}
Proof tree
… (200 of 3730 nodes shown)

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

fn to_refs<'a>(list: &'a mut List) -> &'a mut u32 {
    exists<'r0, 'r1> {
        let result: &'a mut u32;
        'l: loop {
            result = &'r0 mut (*list).value;
            if true {
                let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*list).next);
                list = n;
            } else {
                return result;
            }
        }
    }
}
Proof tree
… (200 of 4134 nodes shown)

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

fn to_refs2<'a>(list: &'a mut List) -> &'a mut u32 {
    exists<'r0, 'r1> {
        let result: &'a mut u32;
        'l: loop {
            result = &'r0 mut (*list).value;
            if true {
                let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*list).next);
                list = n;
            } else {
                break 'l;
            }
        }
        return result;
    }
}
Proof tree
… (200 of 4426 nodes shown)

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

fn to_refs3<'a>(list: &'a mut List) -> &'a mut u32 {
    exists<'r0, 'r1> {
        let result: &'a mut u32;
        let cursor: &'a mut List = &'a mut *list;
        'l: loop {
            result = &'r0 mut (*cursor).value;
            if true {
                let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*cursor).next);
                cursor = n;
            } else {
                return result;
            }
        }
    }
}
Proof tree
… (200 of 4289 nodes shown)

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

fn next<'a>(d: &'a mut Decoder) -> &'a u32 {
    exists<'r0, 'r1> {
        'l: loop {
            let buf: &'r0 u32 = fill_buf::<'r0>(&'r0 mut (*d).buf_read);
            let s: &'r1 u32 = decode::<'r1>(buf);
            if true {
                return s;
            } else {
            }
        }
    }
}
Proof tree
… (200 of 3994 nodes shown)

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

fn next<'s>(f: &'s mut Filter) -> &'s mut u32 {
    exists<'r0, 'r1, 'r2> {
        'l: loop {
            let item: &'r0 mut u32 = iter_next::<'r0>(&'r0 mut (*f).iter);
            if true {
                let keep: bool = call_predicate::<'r1, 'r2>(&'r1 mut (*f).predicate, &'r2 *item);
                if keep {
                    return item;
                } else {
                }
            } else {
                break 'l;
            }
        }
        return no_item::<'s>();
    }
}
Proof tree
… (200 of 5202 nodes shown)

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

fn f() -> u32 {
    exists<'r0> {
        let v: u32 = 0_u32;
        let w: Wrapper<'r0> = Wrapper::<'r0> { value: &'r0 v };
        return *w.value;
    }
}
Proof tree
… (200 of 3603 nodes shown)

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

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

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

fn main() -> () {
    let w: Wrapper<i32> = Wrapper::<i32> { val: 42_i32 };
    println!(w.val);
}

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

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

fn main() -> () {
    let p: Pair = Pair { x: 10_i32, y: 20_i32 };
    exists<'a> {
        let r: & 'a i32 = & 'a p.x;
        println!(*r);
    }
}

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

fn main() -> () {
    let p: Pair = Pair { x: 10_i32, y: 20_i32 };
    exists<'a> {
        let r: & 'a Pair = & 'a p;
        println!((*r).x);
        println!((*r).y);
    }
}

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

fn main() -> () {
    let s: S = S { b: second(), a: first() };
    println!(s.a);
    println!(s.b);
}

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

fn main() -> () {
    let w: Wrap<<S as Value>::Item> = Wrap::<<S as Value>::Item> { value: 7_u32 };
    println!(w.value);
}

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

fn main() -> () {
    let p: Pair = Pair { a: 1_u32, b: 10_u32 };
    p.b += p.a;
    println!(p.b);
}

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);
}

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

fn foo (v1: u32) -> u32 {
    let v2: Dummy = Dummy { value: 1_u32, is_true: false };
    v2.value = 2_u32;
    return v1;
}

Source location: tests/mir_typeck.rs:1142 (all coverage from this test)

fn foo<'a>(v1: &'a Pair) -> u32 {
    exists<'r0> {
        let v2: u32 = (*v1).value;
        return v2;
    }
}

How to read this page