(RigidTy { name: RigidName::AdtId(adt_id), parameters }, state)`

Premise at line 624. Observed failure causes: if_let.

struct field

Line	Coverage	Source
623	✗	(borrow_check_place_expr(env, assumptions, state, prefix) => (prefix_typed, state))
624	1	(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)
629	1	(if field.name == *field_name)
		──────── ("struct field")
631	20	(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, ))

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

Keyboard shortcuts