Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove Kani redundant checks #2579

Open
celinval opened this issue Jul 3, 2023 · 0 comments
Open

Remove Kani redundant checks #2579

celinval opened this issue Jul 3, 2023 · 0 comments
Labels
[C] Bug This is a bug. Something isn't working.

Comments

@celinval
Copy link
Contributor

celinval commented Jul 3, 2023

I tried this code:

// dup.rs
use std::hint::black_box;

#[kani::proof]
fn check_division() {
    black_box(kani::any::<u8>() / kani::any::<u8>());
}

using the following command line invocation:

kani dup.rs

with Kani version: #2551

I expected to see this happen: There should be one division by zero check and one overflow check, and both fail.

Instead, this happened: For the same division, Kani reports 3 different checks of division by zero and 2 overflow checks.

RESULTS:
Check 1: check_division.assertion.1
	 - Status: FAILURE
	 - Description: "attempt to divide by zero"
	 - Location: operations.rs:11:15 in function check_division

Check 2: check_division.assertion.2
	 - Status: FAILURE
	 - Description: "attempt to divide with overflow"
	 - Location: operations.rs:11:15 in function check_division

Check 3: check_division.arithmetic_overflow.1
	 - Status: SUCCESS
	 - Description: "attempt to divide with overflow"
	 - Location: operations.rs:11:15 in function check_division

Check 4: check_division.arithmetic_overflow.2
	 - Status: SUCCESS
	 - Description: "attempt to divide by zero"
	 - Location: operations.rs:11:15 in function check_division

Check 5: check_division.division-by-zero.1
	 - Status: SUCCESS
	 - Description: "division by zero"
	 - Location: operations.rs:11:15 in function check_division

Note: Before the upgrade (#2551), the test above would generate 3 checks. One for overflow and 2 for division by zero.

@celinval celinval added the [C] Bug This is a bug. Something isn't working. label Jul 3, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Bug This is a bug. Something isn't working.
Projects
None yet
Development

No branches or pull requests

1 participant