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

Negative coverage: prove_ty_is_copy / trait / premise env.prove_goal(assumptions, &state, goal) => state

Premise at line 839. Observed failure causes: failed_judgment.

trait
LineCoverageSource
838N/A(let goal = Predicate::is_implemented(TraitId::new("Copy").with(ty, Vec::<Parameter>::new())))
8392(env.prove_goal(assumptions, &state, goal) => state)
──────── ("trait")
8419(prove_ty_is_copy(env, assumptions, state, ty) => state)

2 tests failed proving this premise:

Source location: tests/borrowck.rs:453

fn foo() -> Datum {
    exists<'r0, 'r1> {
        let x: Datum = Datum { value: 0 _ u32 };
        let r: &'r0 Datum = &'r1 x;
        let y: Datum = *r;
        return y;
    }
}
Failed proof tree
… (200 of 1236 nodes shown)

Source location: tests/borrowck.rs:1112

fn foo() -> Datum {
    exists<'r0, 'r1> {
        let x: Datum = Datum { value: 0 _ u32 };
        let r: &mut 'r0 Datum = &mut 'r1 x;
        let y: Datum = *r;
        return y;
    }
}
Failed proof tree
… (200 of 1236 nodes shown)