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: can_outlive / universal target / premise prove(&env.program, &env.env, assumptions, Relation::outlives(param_a, var_b)) => c

Premise at line 81. Observed failure causes: failed_judgment.

universal target
LineCoverageSource
80(if var_b.is_universal())
814(prove(&env.program, &env.env, assumptions, Relation::outlives(param_a, var_b)) => c)
82(if c.unconditionally_true())
──────── ("universal target")
84(can_outlive(env, assumptions, _outlives, param_a, var_b: Variable) => ())

4 tests failed proving this premise:


Source location: tests/borrowck.rs:2170

fn foo<'a, 'b>(v1: &'a u32) -> &'b u32 {
    exists<'r0> {
        let v2: &'r0 u32 = v1;
        return v2;
    }
}
Failed proof tree

Source location: tests/borrowck.rs:2192

fn foo<'a, 'b>(v1: &'a u32, v2: &'b u32) -> () {
    let output: &'b u32 = v2;
    loop {
        output = v1;
    }
}
Failed proof tree

Source location: tests/borrowck.rs:2249

fn foo<'a, 'b, 'c>(v1: &'a u32) -> &'c u32
where
    'a: 'b,
{
    return v1;
}
Failed proof tree

Source location: tests/borrowck.rs:2881

fn foo<'a, 'b>(a: &'a u32) -> &'b u32 {
    let r: &'b u32 = identity::<&'b u32>(a);
    return r;
}
Failed proof tree