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 / binop

binop
LineCoverageSource
4851(borrow_check_expr(env, assumptions, state, lhs, rhs.live_before(env, &state, places_live_on_exit)) => (lhs_ty, state))
486✗(prove_ty_is_rigid(env, assumptions, state, &lhs_ty) => (RigidTy {name: RigidName::ScalarId(scalar), parameters: _}, state))
4871(if scalar.is_int())
4883(borrow_check_expr_has_ty(env, assumptions, state, rhs, &lhs_ty, places_live_on_exit) => state)
──────── ("binop")
49023(borrow_check_expr(env, assumptions, state, Expr::BinOp{lhs, op: _, rhs}, places_live_on_exit) => (lhs_ty, state))

23 tests exercised this rule:

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

fn main() -> () {
    let x: i32 = 1_i32 + 2_i32;
    println!(x);
}
Proof tree
… (200 of 3410 nodes shown)

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

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

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

fn main() -> () {
    println!(sum(1_i32 + 2_i32, sum(3_i32, 4_i32)));
}
Proof tree
… (200 of 3488 nodes shown)

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

fn main() -> () {
    println!(10_i32 - 3_i32);
}
Proof tree
… (200 of 3388 nodes shown)

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

fn main() -> () {
    println!(3_i32 - 10_i32);
}
Proof tree
… (200 of 3388 nodes shown)

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

fn main() -> () {
    println!(10_i32 - 3_i32 - 2_i32);
}
Proof tree
… (200 of 3397 nodes shown)

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

fn main() -> () {
    println!(10_i32 - 3_i32 + 2_i32);
}
Proof tree
… (200 of 3397 nodes shown)

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

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

fn main() -> () {
    println!(10_u32 - 3_u32);
}
Proof tree
… (200 of 3388 nodes shown)

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

fn main() -> () {
    println!(10_i32 - (3_i32 - 2_i32));
}

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

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

fn main() -> () {
    println!(20_i32 - (10_i32 - (3_i32 - 1_i32)));
}

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

fn main() -> () {
    println!(3_i32 * 4_i32);
}

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

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

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

fn main() -> () {
    println!(-3_i32 * 4_i32);
}

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

fn main() -> () {
    println!(3_u32 * 4_u32);
}

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/codegen.rs:1013 (all coverage from this test)

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

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

fn main() -> () {
    println!(20_i32 - 2_i32 * 3_i32);
    println!((20_i32 - 2_i32) * 3_i32);
}

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

How to read this page