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 / assign-op

assign-op
LineCoverageSource
4321(borrow_check_expr(
env,
assumptions,
state,
rhs,
Seq(place, Assignment(place)).live_before(env, &state, places_live_on_exit),
) => (rhs_ty, state))
439N/A(let places_live_before_write = Assignment(place).live_before(env, &state, places_live_on_exit))
441✗(borrow_check_place_expr(env, assumptions, state, place) => (place, state))
442✗(prove_ty_is_rigid(env, assumptions, state, &place.ty) => (RigidTy { name: RigidName::ScalarId(scalar), parameters: _ }, state))
4431(if scalar.is_int())
4441(prove_assignable(env, assumptions, state, rhs_ty, &place.ty) => state)
4462(access_permitted(env, assumptions, state, Access::new(AccessKind::Read, place), places_live_before_write) => state)
4471(access_permitted(env, assumptions, state, Access::new(AccessKind::Write, place), places_live_on_exit) => state)
448N/A(let state = kill_loans(place, state))
──────── ("assign-op")
4507(borrow_check_expr(env, assumptions, state, Expr::AssignOp { place, op: _, rhs }, places_live_on_exit) => (Ty::unit(), state))

7 tests exercised this rule:

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

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

fn bump<'a>(p: &'a mut u32) -> () {
    *p += 1_u32;
}
Proof tree
… (200 of 3509 nodes shown)

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

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

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

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

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

How to read this page