Negative coverage: borrow_check_place_expr / struct field / premise prove_ty_is_rigid(env, assumptions, state, &prefix_typed.ty) => (RigidTy { name: RigidName::AdtId(adt_id), parameters }, state)
Premise at line 584. Observed failure causes: if_let.
struct field| Line | Coverage | Source |
|---|---|---|
| 583 | ✗ | (borrow_check_place_expr(env, assumptions, state, prefix) => (prefix_typed, state)) |
| 584 | 1 | (prove_ty_is_rigid(env, assumptions, state, &prefix_typed.ty) => (RigidTy { name: RigidName::AdtId(adt_id), parameters }, state)) |
| 585 | ✗ | (let Struct { id: _, binder } = env.crates().struct_named(&adt_id)?) |
| 586 | ✗ | (let StructBoundData { where_clauses, fields } = binder.instantiate_with(¶meters)?) |
| 587 | ✗ | (prove_where_clauses(env, assumptions, state, where_clauses) => state) |
| 588 | ✗ | (field in fields) |
| 589 | 1 | (if field.name == *field_name) |
| ──────── ("struct field") | ||
| 591 | 7 | (borrow_check_place_expr(env, assumptions, state, PlaceExpr::Field { prefix, field_name }) => ( TypedPlaceExpr::new(&field.ty, TypedPlaceExpressionData::field(prefix_typed, field_name)), state, )) |
1 test failed proving this premise:
Source location: tests/mir_typeck.rs:613
fn foo (v1: u32) -> u32 {
let v2: Dummy = Dummy { value: 1 _ u32 };
v1.value = 2 _ u32;
return v1;
}Failed proof tree
check_all_crates failedmod.rs:41rule "check all prefixes"mod.rs:53check_crate failedmod.rs:60rule "check crate"mod.rs:73check_crate_item failedmod.rs:163rule "free fn"mod.rs:191check_free_fn failedfns.rs:14rule "check free fn"fns.rs:24check_fn failedfns.rs:31rule "check fn"fns.rs:55check_fn_body failedfns.rs:62rule "expr fn body"fns.rs:90borrow_check failednll.rs:126rule "borrow_check"nll.rs:137borrow_check_block failednll.rs:144rule "basic block"nll.rs:159borrow_check_statement failednll.rs:176rule "expr"nll.rs:229borrow_check_expr failednll.rs:340rule "assign"nll.rs:362borrow_check_place_expr failednll.rs:563rule "struct field"nll.rs:584 (failed: if_let)