premise `if field.name == *field_name`

Premise at line 589. Observed failure causes: if_false.

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(&parameters)?)
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:595

fn foo (v1: u32) -> u32 {
    let v2: Dummy = Dummy { value: 1 _ u32 };
    v2.nonexistent = 2 _ u32;
    return v1;
}

Failed proof tree

Keyboard shortcuts