Positive coverage: prove_sub / normalize-r

4 tests exercised this rule:

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

fn foo () -> u32 {
    exists<'l_p, 'l_q, 'loan_0, 'loan_1, 'loan_2, 'loan_3> {
        let a: u32 = 0_u32;
        let b: u32 = 0_u32;
        // In Rustc, the 1-tuple is needed for some reason
        // Niko does not 100% understand, else rustc is able to
        // see that this program is safe.
        let q: &'l_q mut u32 = &'loan_0 mut a;
        let p: &'l_p mut u32 = &'loan_1 mut a;
        if true {
            p = &'loan_1 mut a;
            q = &'loan_2 mut b;
        } else {
            p = &'loan_3 mut b;
        }
        *q = 1_u32;
        return *p;
    }
}

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

fn foo() -> u32 {
    exists<'r0, 'r1, 'r2, 'r3> {
        let p: Point = Point { x: 0_u32, y: 0_u32 };
        let b1: &'r0 mut u32 = &'r1 mut p.x;
        let b2: &'r2 mut u32 = &'r3 mut p.y;
        *b1 = 1_u32;
        *b2 = 2_u32;
        return 0_u32;
    }
}

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

fn remove_last_node_recursive<'a>(node: &'a mut List) -> u32 {
    exists<'r0> {
        let next: &'r0 mut List = next_of::<'r0>(&'r0 mut *node);
        if true {
            remove_last_node_recursive::<'r0>(next);
        } else {
            *node = List { value: 0_u32 };
        }
        return 0_u32;
    }
}

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

fn remove_last_node_iterative<'a>(node: &'a mut List) -> u32 {
    exists<'r0, 'r1> {
        let cursor: &'r0 mut List = &'r0 mut *node;
        'l: loop {
            let next: &'r1 mut List = &'r1 mut *cursor;
            if true {
                cursor = next;
            } else {
                break 'l;
            }
        }
        *cursor = List { value: 0_u32 };
        return 0_u32;
    }
}