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
623✗(borrow_check_place_expr(env, assumptions, state, prefix) => (prefix_typed, state))
6241(prove_ty_is_rigid(env, assumptions, state, &prefix_typed.ty) => (RigidTy { name: RigidName::AdtId(adt_id), parameters }, state))
625✗(let Struct { id: _, binder } = env.crates().struct_named(&adt_id)?)
626✗(let StructBoundData { where_clauses, fields } = binder.instantiate_with(&parameters)?)
627✗(prove_where_clauses(env, assumptions, state, where_clauses) => state)
628✗(field in fields)
6291(if field.name == *field_name)
──────── ("struct field")
63112(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,
))

12 tests exercised this rule:

Source location: tests/borrowck.rs:412 (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 1156 nodes shown)

Source location: tests/borrowck.rs:2499 (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 1282 nodes shown)

Source location: tests/borrowck.rs:3240 (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 1340 nodes shown)

Source location: tests/borrowck.rs:4108 (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 1733 nodes shown)

Source location: tests/borrowck.rs:4143 (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 2021 nodes shown)

Source location: tests/borrowck.rs:4190 (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 1888 nodes shown)

Source location: tests/borrowck.rs:4233 (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 1596 nodes shown)

Source location: tests/borrowck.rs:4356 (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 2783 nodes shown)

Source location: tests/codegen.rs:141 (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 1068 nodes shown)

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

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

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

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

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

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