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_statement / expr

expr
LineCoverageSource
23226(borrow_check_expr(
env,
assumptions,
state,
expr,
places_live_on_exit
) => (_init_ty, state))
──────── ("expr")
24047(borrow_check_statement(env, assumptions, state, Stmt::Expr { expr }, places_live_on_exit) => (env, state))

47 tests exercised this rule:

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

fn foo() -> Datum {
    let x: Datum = Datum { value: 0_u32 };
    let y: Datum = x;
    x = Datum { value: 1_u32 };
    let z: Datum = x;
    return z;
}
Proof tree
… (200 of 3504 nodes shown)

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

fn foo() -> u32 {
    let x: u32;
    if true {
        x = 1_u32;
    } else {
        x = 2_u32;
    }
    return x;
}
Proof tree
… (200 of 3440 nodes shown)

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

fn foo() -> u32 {
    let x: u32 = 1_u32;
    if true {
        x = 2_u32;
    }
    return x;
}
Proof tree
… (200 of 3432 nodes shown)

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

fn foo() -> i32 {
    exists<'r0, 'r1> {
        let result: i32;
        {
            let v1: i32 = 22_i32;
            let v2: &'r0 i32 = &'r1 v1;
            result = *v2;
        }
        return result;
    }
}
Proof tree
… (200 of 3630 nodes shown)

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

fn min_problem_case_4<'a>(list: &'a mut Map, list2: &'a mut Map) -> u32 {
    exists<'r0> {
        let num: &'r0 mut u32 = &'r0 mut (*list).value;
        list = &'a mut *list2;
        num;
        return 0_u32;
    }
}
Proof tree
… (200 of 3676 nodes shown)

Source location: tests/borrowck.rs:2963 (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;
    }
}
Proof tree
… (200 of 3956 nodes shown)

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

fn bar() -> u32 {
    exists<'r0, 'r1> {
        let v: u32 = 1_u32;
        let p: &'r0 u32 = &'r1 v;
        foo(0_u32);
        return *p;
    }
}
Proof tree
… (200 of 3633 nodes shown)

Source location: tests/borrowck.rs:3568 (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;
    }
}
Proof tree
… (200 of 3730 nodes shown)

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

fn foo() -> u32 {
    exists<'r0, 'r1, 'r2> {
        let x: u32 = 22_u32;
        let p: &'r1 u32 = &'r0 x;
        let q: &'r2 u32 = p;
        x = 1_u32;
        return 0_u32;
    }
}
Proof tree
… (200 of 3521 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:4167 (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;
    }
}

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

Source location: tests/borrowck.rs:4214 (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;
    }
}

Source location: tests/borrowck.rs:4276 (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;
    }
}

Source location: tests/borrowck.rs:4326 (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;
    }
}

Source location: tests/borrowck.rs:4415 (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;
    }
}

Source location: tests/borrowck.rs:4467 (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;
            }
        }
    }
}

Source location: tests/borrowck.rs:4502 (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;
    }
}

Source location: tests/borrowck.rs:4549 (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;
            }
        }
    }
}

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

fn foo() -> u32 {
    let a: u32 = 0_u32;
    a;
    a;
    return 0_u32;
}

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

fn foo() -> u32 {
    exists<'l0> {
        let a: u32 = 0_u32;
        let p: &'l0 u32 = &'l0 a;
        let q: &'l0 u32 = p;
        let r: &'l0 u32 = p;
        p;
        return 0_u32;
    }
}

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

fn foo() -> () {
    let x: u32 = 1_u32;
    exists<'r0> {
        let r: &'r0 mut u32 = &'r0 mut x;
        x += *r;
    }
}

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

fn bump<'a>(p: &'a mut u32) -> () {
    *p += 1_u32;
}

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

fn main() -> () {
    let x: i32 = 1_i32;
    x = 2 _ i32;
    println!(x);
}

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

fn main() -> () {
    a();
}

Source location: tests/codegen.rs:469 (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:485 (all coverage from this test)

fn main() -> () {
    let x: i32 = 1_i32;
    exists<'a> {
        let r: &'a mut i32 = &'a mut x;
        *r = 2_i32;
        println!(*r);
    }
}

Source location: tests/codegen.rs:532 (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:550 (all coverage from this test)

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

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

fn main() -> () {
    let x: u32 = 1_u32;
    exists<'a> {
        let r: &'a mut u32 = &'a mut x;
        let amount: u32 = update::<'a>(r);
        println!(amount);
    }
}

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

fn main() -> () {
    let x: u32 = 0_u32;
    x = 1_u32 + 2_u32 + 3_u32;
    println!(x);
}

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

fn main() -> () {
    let x: i32 = 10_i32;
    (x = (x - 3_i32));
    println!(x);
}

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

fn main() -> () {
    let x: u32 = 1_u32;
    exists<'a> {
        let r: &'a mut u32 = &'a mut x;
        x += update::<'a>(r);
    }
    println!(x);
}

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

fn main() -> () {
    let x: u32 = 1_u32;
    x += 2_u32 + 3_u32;
    println!(x);
}

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

fn main() -> () {
    let p: Pair = Pair { a: 1_u32, b: 10_u32 };
    p.b += p.a;
    println!(p.b);
}

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

fn main() -> () {
    let x: u32 = 20_u32;
    x -= 2_u32 + 3_u32;
    println!(x);
}

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

fn main() -> () {
    let p: Pair = Pair { a: 2_u32, b: 3_u32 };
    p.b *= p.a + 4_u32;
    println!(p.b);
    println!(p.a);
}

Source location: tests/consts.rs:166 (all coverage from this test)

Source location: tests/functions.rs:70 (all coverage from this test)

fn main() {
    helper();
}

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:259 (all coverage from this test)

fn foo (v1: u32) -> u32 {
    let v2: Dummy = Dummy { value: 1_u32, is_true: false };
    v2.value = 2_u32;
    return v1;
}

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

fn main() -> () { require_marker::<u32>; }
}])
tc_ok()
);
}

#[test]
fn_value_with_forwarded_trait_bound() {
alityTest::new(crates![crate Foo {
trait Marker {}
impl Marker for u32 {}
fn require<T>() -> () where T: Marker {}
fn outer<T>() -> () where T: Marker { require::<T>; }
fn main() -> () { outer::<u32>(); }
}])
tc_ok()
);
}

#[test]
bare_fn_value_with_satisfied_where_clause() {
alityTest::new(crates![crate Foo {
trait Marker {}
impl Marker for u32 {}
fn require() -> () where u32: Marker {}
fn main() -> () { require; }
}])
tc_ok()
);
}

#[test]
fn_value_with_forwarded_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () where 'a: 'b { require::<'a, 'b>; }
fn main() -> () { outer::<'static, 'static>(); }
}])
tc_ok()
);
}

#[test]
fn_value_with_unsatisfied_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () { require::<'a, 'b>; }
fn main() -> () {}
}])
tc_err(expect_test::expect![[r#"
error: lifetime may not live long enough
 --> lib.rs
  |
7 | pub fn outer<'a00, 'a01>() -> () {
  |              ----  ---- lifetime `'a01` defined here
  |              |
  |              lifetime `'a00` defined here
8 |     require::<'a00, 'a01>;
  |     ^^^^^^^^^^^^^^^^^^^^^ requires that `'a00` must outlive `'a01`
  |
  = help: consider adding the following bound: `'a00: 'a01`

error: could not compile `Foo` (lib) due to 1 previous error
)
(expect_test::expect!["crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"]);
}

ound assignment of an integer of a different type should fail.
#[test]
compound_add_mismatched_int_types() {
alityTest::new(crates![crate Foo {
fn foo() -> () {
    let x: u32 = 1_u32;
    x += 2_u8;
}

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

fn main() -> () { outer::<u32>(); }
}])
tc_ok()
);
}

#[test]
bare_fn_value_with_satisfied_where_clause() {
alityTest::new(crates![crate Foo {
trait Marker {}
impl Marker for u32 {}
fn require() -> () where u32: Marker {}
fn main() -> () { require; }
}])
tc_ok()
);
}

#[test]
fn_value_with_forwarded_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () where 'a: 'b { require::<'a, 'b>; }
fn main() -> () { outer::<'static, 'static>(); }
}])
tc_ok()
);
}

#[test]
fn_value_with_unsatisfied_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () { require::<'a, 'b>; }
fn main() -> () {}
}])
tc_err(expect_test::expect![[r#"
error: lifetime may not live long enough
 --> lib.rs
  |
7 | pub fn outer<'a00, 'a01>() -> () {
  |              ----  ---- lifetime `'a01` defined here
  |              |
  |              lifetime `'a00` defined here
8 |     require::<'a00, 'a01>;
  |     ^^^^^^^^^^^^^^^^^^^^^ requires that `'a00` must outlive `'a01`
  |
  = help: consider adding the following bound: `'a00: 'a01`

error: could not compile `Foo` (lib) due to 1 previous error
)
(expect_test::expect!["crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"]);
}

ound assignment of an integer of a different type should fail.
#[test]
compound_add_mismatched_int_types() {
alityTest::new(crates![crate Foo {
fn foo() -> () {
    let x: u32 = 1_u32;
    x += 2_u8;
}

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

fn main() -> () { require; }
}])
tc_ok()
);
}

#[test]
fn_value_with_forwarded_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () where 'a: 'b { require::<'a, 'b>; }
fn main() -> () { outer::<'static, 'static>(); }
}])
tc_ok()
);
}

#[test]
fn_value_with_unsatisfied_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () { require::<'a, 'b>; }
fn main() -> () {}
}])
tc_err(expect_test::expect![[r#"
error: lifetime may not live long enough
 --> lib.rs
  |
7 | pub fn outer<'a00, 'a01>() -> () {
  |              ----  ---- lifetime `'a01` defined here
  |              |
  |              lifetime `'a00` defined here
8 |     require::<'a00, 'a01>;
  |     ^^^^^^^^^^^^^^^^^^^^^ requires that `'a00` must outlive `'a01`
  |
  = help: consider adding the following bound: `'a00: 'a01`

error: could not compile `Foo` (lib) due to 1 previous error
)
(expect_test::expect!["crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"]);
}

ound assignment of an integer of a different type should fail.
#[test]
compound_add_mismatched_int_types() {
alityTest::new(crates![crate Foo {
fn foo() -> () {
    let x: u32 = 1_u32;
    x += 2_u8;
}

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

fn main() -> () { outer::<'static, 'static>(); }
}])
tc_ok()
);
}

#[test]
fn_value_with_unsatisfied_lifetime_bound() {
alityTest::new(crates![crate Foo {
fn require<'a, 'b>() -> () where 'a: 'b {}
fn outer<'a, 'b>() -> () { require::<'a, 'b>; }
fn main() -> () {}
}])
tc_err(expect_test::expect![[r#"
error: lifetime may not live long enough
 --> lib.rs
  |
7 | pub fn outer<'a00, 'a01>() -> () {
  |              ----  ---- lifetime `'a01` defined here
  |              |
  |              lifetime `'a00` defined here
8 |     require::<'a00, 'a01>;
  |     ^^^^^^^^^^^^^^^^^^^^^ requires that `'a00` must outlive `'a01`
  |
  = help: consider adding the following bound: `'a00: 'a01`

error: could not compile `Foo` (lib) due to 1 previous error
)
(expect_test::expect!["crates/formality-rust/src/prove/prove_outlives.rs:8:1: no applicable rules for prove_outlives { a: !lt_0, b: !lt_1, assumptions: {}, env: Env { variables: [!lt_0, !lt_1], bias: Soundness, pending: [], allow_pending_outlives: false } }"]);
}

ound assignment of an integer of a different type should fail.
#[test]
compound_add_mismatched_int_types() {
alityTest::new(crates![crate Foo {
fn foo() -> () {
    let x: u32 = 1_u32;
    x += 2_u8;
}

Source location: tests/sized_trait.rs:142 (all coverage from this test)

Source location: tests/traits.rs:11 (all coverage from this test)

fn main() -> () { require_copy::<i128>(); }
}])
p_execute()
tc_ok()
);
}

#[test]
is_copy() {
alityTest::new(crates![crate test {
fn require_copy<T>() -> () where T: Copy { trusted }
fn main() -> () { require_copy::<u128>(); }
}])
p_execute()
tc_ok()
);
}

#[test]
_with_valid_fn() {
alityTest::new(crates![
crate core {
    trait A {
        fn a() -> ();
    }
}

Source location: tests/traits.rs:22 (all coverage from this test)

fn main() -> () { require_copy::<u128>(); }
}])
p_execute()
tc_ok()
);
}

#[test]
_with_valid_fn() {
alityTest::new(crates![
crate core {
    trait A {
        fn a() -> ();
    }
}

How to read this page