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_expr / false

false
LineCoverageSource
──────── ("false")
4627(borrow_check_expr(_env, _assumptions, state, Expr::False, _places_live_on_exit) => (ScalarId::Bool, state))

7 tests exercised this rule:

Source location: tests/borrowck.rs:2831

#[test]
fn if_false_borrowck() {
    FormalityTest::new(feature_gate_program(NLL_GATE, IF_FALSE_BORROWCK))
        .skip_execute()
        .err(expect_test::expect![[r#"
            the rule "borrow of disjoint places" at (nll.rs) failed because
              condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
                &loan.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
                &access.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target

            the rule "loan_cannot_outlive" at (nll.rs) failed because
              condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
                outlived_by_loan = {!lt_1, ?lt_2, ?lt_3}
                &lifetime.upcast() = !lt_1

            the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
              condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
              {
                  Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
                  {
                      Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
                      Lt::Variable(Variable::ExistentialVar(_)) => true,
                      Lt::Variable(Variable::BoundVar(_)) =>
                      panic!("cannot outlive a bound var"), Lt::Erased => true,
                  }, Parameter::Const(_) => panic!("cannot outlive a constant"),
              })`

            the rule "write-indirect" at (nll.rs) failed because
              pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `m`

            the rule "write-indirect" at (nll.rs) failed because
              condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
                place_accessed = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
                place_loaned_ref = m : &!lt_1 mut Map"#]]);

    FormalityTest::new(feature_gate_program(POLONIUS_ALPHA_GATE, IF_FALSE_BORROWCK))
        .skip_execute()
        .ok();

    FormalityTest::new(feature_gate_program(
        POLONIUS_UNLOCKED_GATE,
        IF_FALSE_BORROWCK,
    ))
    .skip_execute()
    .ok();
}
Proof tree
… (200 of 1377 nodes shown)

Source location: tests/borrowck.rs:2838

#[test]
fn if_false_borrowck() {
    FormalityTest::new(feature_gate_program(NLL_GATE, IF_FALSE_BORROWCK))
        .skip_execute()
        .err(expect_test::expect![[r#"
            the rule "borrow of disjoint places" at (nll.rs) failed because
              condition evaluated to false: `place_disjoint_from_place(&loan.place, &access.place)`
                &loan.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
                &access.place = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target

            the rule "loan_cannot_outlive" at (nll.rs) failed because
              condition evaluated to false: `!outlived_by_loan.contains(&lifetime.upcast())`
                outlived_by_loan = {!lt_1, ?lt_2, ?lt_3}
                &lifetime.upcast() = !lt_1

            the rule "loan_not_required_by_universal_regions" at (nll.rs) failed because
              condition evaluated to false: `outlived_by_loan.iter().all(|p| match p
              {
                  Parameter::Ty(_) => false, Parameter::Lt(lt) => match lt.as_ref()
                  {
                      Lt::Static => false, Lt::Variable(Variable::UniversalVar(_)) => false,
                      Lt::Variable(Variable::ExistentialVar(_)) => true,
                      Lt::Variable(Variable::BoundVar(_)) =>
                      panic!("cannot outlive a bound var"), Lt::Erased => true,
                  }, Parameter::Const(_) => panic!("cannot outlive a constant"),
              })`

            the rule "write-indirect" at (nll.rs) failed because
              pattern `TypedPlaceExpressionData::Deref(place_loaned_ref)` did not match value `m`

            the rule "write-indirect" at (nll.rs) failed because
              condition evaluated to false: `place_accessed.is_prefix_of(place_loaned_ref)`
                place_accessed = *(m : &!lt_1 mut Map) : <&!lt_1 mut Map as Derefable>::Target
                place_loaned_ref = m : &!lt_1 mut Map"#]]);

    FormalityTest::new(feature_gate_program(POLONIUS_ALPHA_GATE, IF_FALSE_BORROWCK))
        .skip_execute()
        .ok();

    FormalityTest::new(feature_gate_program(
        POLONIUS_UNLOCKED_GATE,
        IF_FALSE_BORROWCK,
    ))
    .skip_execute()
    .ok();
}
Proof tree
… (200 of 1350 nodes shown)

Source location: tests/codegen.rs:24

fn main() -> () {
    println!(1_i32);
    println!(true);
    println!(false);
}
Proof tree
… (200 of 995 nodes shown)

Source location: tests/codegen.rs:377

fn main() -> () {
    let x: i32 = 0_i32;
    'a: loop {
        if false {
            x = 1_i32;
            break 'a;
        } else {
            x = 2_i32;
            break 'a;
        }
    }
    println!(x);
}
Proof tree
… (200 of 1113 nodes shown)

Source location: tests/mir_typeck.rs:35

fn foo () -> u8 {
    let v1: u16 = 5_u16;
    let v2: u32 = 5_u32;
    let v3: u64 = 5_u64;
    let v4: usize = 5_usize;
    let v5: i8 = 5_i8;
    let v6: i16 = 5_i16;
    let v7: i32 = 5_i32;
    let v8: i64 = 5_i64;
    let v9: isize = 5_isize;
    let v10: bool = false;
    return 5_u8;
}
Proof tree
… (200 of 1175 nodes shown)

Source location: tests/mir_typeck.rs:234

fn foo (v1: u32) -> u32 {
    let v2: Dummy = Dummy { value: 1_u32, is_true: false };
    v2.value = 2_u32;
    return v1;
}
Proof tree
… (200 of 1079 nodes shown)

Source location: tests/mir_typeck.rs:670

fn foo() -> bool {
    let v1: bool = false;
    return v1;
}
Proof tree
… (200 of 1018 nodes shown)