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

Positive coverage: can_outlive / universal target

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

3 tests exercised this rule:

Source location: tests/borrowck.rs:2768 (all coverage from this test)

fn foo<'a, 'b>(v1: &'a u32) -> &'b u32
where
    'a: 'b,
{
    exists<'r0> {
        let v2: &'r0 u32 = v1;
        return v2;
    }
}
Proof tree
… (200 of 3490 nodes shown)

Source location: tests/borrowck.rs:4048 (all coverage from this test)

fn foo<'a, 'b>(p: &'a mut u32) -> u32 where 'a: 'b {
    let q: &'b mut u32 = &'b mut *p;
    q;
    return 0 _ u32;
}
Proof tree
… (200 of 3546 nodes shown)

Source location: tests/borrowck.rs:4896 (all coverage from this test)

fn use_it_but_its_the_same_region<'a, 'b>() -> u32 where 'a: 'b, 'b: 'a {
    exists<'r0> {
        let v: Invariant<'r0> = create_invariant::<'r0>();
        if true {
            return sink::<'a, 'r0>(v);
        } else {
            return sink::<'b, 'r0>(v);
        }
    }
}
Proof tree
… (200 of 3604 nodes shown)

How to read this page