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: borrow_check_loop / fixed-point

fixed-point
LineCoverageSource
5959(borrow_check_block(env, assumptions, state0, body, places_live_on_exit) => state1)
5963(if state0 == state1)
──────── ("fixed-point")
59822(borrow_check_loop(env, assumptions, state0, body, places_live_on_exit) => state1)

22 tests exercised this rule:

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

fn foo() -> u32 {
    exists<'r0, 'r1> {
        'a: loop {
            let x: i32 = 0_i32;
            let r: &'r0 i32 = &'r1 x;
            let _y: i32 = *r;
            continue 'a;
        }
    }
}
Proof tree
… (200 of 1457 nodes shown)

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;
    }
}
Proof tree
… (200 of 1847 nodes shown)

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

fn no_control_flow() -> u32 {
    exists<'r0, 'r1, 'r2, 'r3> {
        let b: X = X { value: 0_u32 };
        let p: &'r0 mut X = &'r1 mut b;
        'l: loop {
            let now: &'r2 mut X = &'r2 mut *p;
            if true {
                let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *now);
                p = next;
            } else {
                break 'l;
            }
        }
        return 0_u32;
    }
}
Proof tree
… (200 of 2276 nodes shown)

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

fn conditional() -> u32 {
    exists<'r0, 'r1, 'r2, 'r3> {
        let b: X = X { value: 0_u32 };
        let p: &'r0 mut X = &'r1 mut b;
        'l: loop {
            let now: &'r2 mut X = &'r2 mut *p;
            if true {
                if true {
                    let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *now);
                    p = next;
                } else {
                }
            } else {
                break 'l;
            }
        }
        return 0_u32;
    }
}
Proof tree
… (200 of 2332 nodes shown)

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

fn conditional_with_indirection() -> u32 {
    exists<'r0, 'r1, 'r2, 'r3> {
        let b: X = X { value: 0_u32 };
        let p: &'r0 mut X = &'r1 mut b;
        'l: loop {
            let now: &'r2 mut X = &'r2 mut *p;
            if true {
                if true {
                    let next: &'r3 mut X = next_of::<'r3>(&'r3 mut *p);
                    p = next;
                } else {
                }
            } else {
                break 'l;
            }
        }
        return 0_u32;
    }
}
Proof tree
… (200 of 2450 nodes shown)

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

fn to_refs<'a>(list: &'a mut List) -> &'a mut u32 {
    exists<'r0, 'r1> {
        let result: &'a mut u32;
        'l: loop {
            result = &'r0 mut (*list).value;
            if true {
                let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*list).next);
                list = n;
            } else {
                return result;
            }
        }
    }
}
Proof tree
… (200 of 1733 nodes shown)

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

fn to_refs2<'a>(list: &'a mut List) -> &'a mut u32 {
    exists<'r0, 'r1> {
        let result: &'a mut u32;
        'l: loop {
            result = &'r0 mut (*list).value;
            if true {
                let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*list).next);
                list = n;
            } else {
                break 'l;
            }
        }
        return result;
    }
}
Proof tree
… (200 of 2021 nodes shown)

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

fn to_refs3<'a>(list: &'a mut List) -> &'a mut u32 {
    exists<'r0, 'r1> {
        let result: &'a mut u32;
        let cursor: &'a mut List = &'a mut *list;
        'l: loop {
            result = &'r0 mut (*cursor).value;
            if true {
                let n: &'r1 mut List = next_from_field::<'r1>(&'r1 mut (*cursor).next);
                cursor = n;
            } else {
                return result;
            }
        }
    }
}
Proof tree
… (200 of 1888 nodes shown)

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

fn next<'a>(d: &'a mut Decoder) -> &'a u32 {
    exists<'r0, 'r1> {
        'l: loop {
            let buf: &'r0 u32 = fill_buf::<'r0>(&'r0 mut (*d).buf_read);
            let s: &'r1 u32 = decode::<'r1>(buf);
            if true {
                return s;
            } else {
            }
        }
    }
}
Proof tree
… (200 of 1596 nodes shown)

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

fn next<'s>(f: &'s mut Filter) -> &'s mut u32 {
    exists<'r0, 'r1, 'r2> {
        'l: loop {
            let item: &'r0 mut u32 = iter_next::<'r0>(&'r0 mut (*f).iter);
            if true {
                let keep: bool = call_predicate::<'r1, 'r2>(&'r1 mut (*f).predicate, &'r2 *item);
                if keep {
                    return item;
                } else {
                }
            } else {
                break 'l;
            }
        }
        return no_item::<'s>();
    }
}
Proof tree
… (200 of 2783 nodes shown)

Source location: tests/codegen.rs:110 (all coverage from this test)

fn main() -> () {
    let x: i32 = 0_i32;
    'a: loop {
        println!(x);
        break 'a;
    }
}

Proof trees omitted for the remaining 12 tests; each one is on its test’s page in Coverage by test.

Source location: tests/codegen.rs:318 (all coverage from this test)

fn main() -> () {
    let x: i32 = 0_i32;
    'a: loop {
        if true {
            println!(x);
            break 'a;
        } else {
            continue 'a;
        }
    }
}

Source location: tests/codegen.rs:336 (all coverage from this test)

fn main() -> () {
    'outer: loop {
        println!(1_i32);
        'inner: loop {
            println!(2_i32);
            break 'outer;
        }
    }
    println!(3_i32);
}

Source location: tests/codegen.rs:356 (all coverage from this test)

fn main() -> () {
    'a: loop {
        if true {
            println!(1_i32);
            break 'a;
        } else {
            println!(2_i32);
            break 'a;
        }
    }
    println!(3_i32);
}

Source location: tests/codegen.rs:377 (all coverage from this test)

fn main() -> () {
    let x: i32 = 0_i32;
    'a: loop {
        if false {
            x = 1_i32;
            break 'a;
        } else {
            x = 2_i32;
            break 'a;
        }
    }
    println!(x);
}

Source location: tests/codegen.rs:443 (all coverage from this test)

fn main() -> () {
    let x: i32 = 0_i32;
    'a: loop {
        x = 77_i32;
        break 'a;
    }
    println!(x);
}

Source location: tests/codegen.rs:461 (all coverage from this test)

fn main() -> () {
    let x: i32 = 0_i32;
    'a: loop {
        {
            x = 88_i32;
            break 'a;
        }
    }
    println!(x);
}

Source location: tests/mir_typeck.rs:110 (all coverage from this test)

fn foo() -> u32 {
    let v0: u32 = 0_u32;
    loop {
        v0 = v0;
    }
}

Source location: tests/mir_typeck.rs:988 (all coverage from this test)

fn foo() -> u32 {
    'a: loop {
        break 'a;
    }
    return 0_u32;
}

Source location: tests/mir_typeck.rs:1047 (all coverage from this test)

fn foo() -> u32 {
    'a: loop {
        continue 'a;
    }
    return 0_u32;
}

Source location: tests/return_validation.rs:84 (all coverage from this test)

fn foo() -> u32 {
    loop {
    }
}

Source location: tests/return_validation.rs:118 (all coverage from this test)

fn foo() -> u32 {
    'a: loop {
        break 'a;
    }
    return 0_u32;
}