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_fn_ref / fn-ref

fn-ref
LineCoverageSource
6291(let Fn { binder, .. } = env.crates().fn_named(id)?)
6302(if binder.len() == args.len())
631✗(let FnBoundData { where_clauses, .. } = binder.instantiate_with(args)?)
6325(prove_where_clauses(env, assumptions, state, where_clauses) => state)
633N/A(let ty = Ty::rigid(RigidName::fn_def(id), args))
──────── ("fn-ref")
63543(borrow_check_fn_ref(env, assumptions, state, id, args) => (ty, state))

43 tests exercised this rule:

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

fn foo<'a>(a: &'a u32) -> &'a u32 {
    exists<'r0> {
        let r: &'r0 u32 = identity::<&'r0 u32>(a);
        return r;
    }
}
Proof tree
… (200 of 3532 nodes shown)

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

fn bar() -> u32 {
    exists<'r1> {
        let v: u32 = 7_u32;
        let r: u32 = foo::<'r1>(&'r1 v);
        return r;
    }
}
Proof tree
… (200 of 3624 nodes shown)

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

fn foo<'a, 'b>(a: &'a u32) -> &'b u32
where
    'a: 'b,
{
    let r: &'b u32 = identity::<&'b u32>(a);
    return r;
}
Proof tree
… (200 of 3524 nodes shown)

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

fn foo<'b>(a: &'b u32) -> &'b u32 {
    let r: &'b u32 = bar::<'b, &'b u32>(a);
    return r;
}
Proof tree
… (200 of 3540 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: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 tree
… (200 of 3837 nodes shown)

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

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

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

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

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;
    }
}

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

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:4592 (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 {
            }
        }
    }
}

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

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

fn use_it<'a, 'b>() -> u32 {
    exists<'r0> {
        let v: Invariant<'r0> = create_invariant::<'r0>();
        if true {
            return sink::<'a, 'r0>(v);
        } else {
            return sink::<'b, 'r0>(v);
        }
    }
}

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);
        }
    }
}

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

fn main() -> () {
    let y: i32 = add_one(1_i32);
    println!(y);
}

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

fn main() -> () {
    let y: i32 = identity::<i32>(42_i32);
    println!(y);
}

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

fn main() -> () {
    let a: i32 = f(1_i32);
    let b: i32 = f(2_i32);
    let c: i32 = f(3_i32);
    println!(a);
    println!(b);
    println!(c);
}

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

fn main() -> () {
    let y: i32 = f(f(42_i32));
    println!(y);
}

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

fn main() -> () {
    let r: i32 = outer(7_i32);
    println!(r);
}

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

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

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

fn main() -> () {
    let r: i32 = first::<i32, bool>(10_i32, true);
    println!(r);
}

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

fn main() -> () {
    println!(identity::<S>(7_u32));
}

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

fn main() -> () { println!(left() + right()); }
}])
tc_ok()
ect_output("1\n2\n30\n")
)
}

#[test]
ion_in_call_arguments() {
alityTest::new(crates![crate test {
fn sum(x: i32, y: i32) -> i32 { return x + y; }
fn main() -> () {
    println!(sum(1_i32 + 2_i32, sum(3_i32, 4_i32)));
}

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

fn main() -> () {
    println!(sum(1_i32 + 2_i32, sum(3_i32, 4_i32)));
}

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

fn main() -> () {
    let s: S = S { b: second(), a: first() };
    println!(s.a);
    println!(s.b);
}

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

fn main() -> () { println!(left() - right()); }
}])
tc_ok()
ect_output("1\n2\n7\n")
);
}

#[test]
er_subtraction_unsigned() {
alityTest::new(crates![crate Foo {
fn main() -> () {
    println!(10_u32 - 3_u32);
}

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

fn main() -> () {
    println!(identity::<Number>(7_u32));
    println!(identity::<Flag>(true));
    println!(identity::<Number>(9_u32));
}

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

fn main() -> () { println!(left() * right()); }
}])
tc_ok()
ect_output("1\n2\n12\n")
);
}

#[test]
plication_with_parentheses() {
alityTest::new(crates![crate Foo {
fn main() -> () {
    println!((2_i32 + 3_i32) * 4_i32);
    println!(2_i32 * (3_i32 + 4_i32));
}

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

fn bar(v1: u32) -> u32 {
    let v0: u32 = foo(v1);
    return v0;
}

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

fn bar(v1: u32) -> u32 {
    let v0: u32 = identity::<u32>(v1);
    return v0;
}

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