Spurious failure on leading_zeros

[zhassan-aws]

This failure only occurs with the next, not-yet-integrated version of CBMC (5.52.0). This may be related to diffblue/cbmc#6703.

I tried this code:

fn main() {
    let x: u64 = 0;
    let _ = x.leading_zeros();
}

using the following command line invocation:

kani test.rs

with Kani version: 53f15955016 but with CBMC 5.52.0

I expected to see this happen: Verification successful

Instead, this happened: Verification failed:

CBMC 5.52.0 (cbmc-5.52.0)
CBMC version 5.52.0 (cbmc-5.52.0) 64-bit x86_64 linux
<snip>
Check 2: bit_count.1
         - Status: FAILURE
         - Description: "count leading zeros is undefined for value zero in __builtin_clz(var_3)"

Check 3: core::num::<impl u64>::leading_zeros.overflow.1
         - Status: SUCCESS
         - Description: "arithmetic overflow on unsigned to unsigned type conversion in (unsigned int)var_2"
<snip>

SUMMARY: 
 ** 1 of 4 failed
Failed Checks: count leading zeros is undefined for value zero in __builtin_clz(var_3)

VERIFICATION:- FAILED

Running it with rustc produces no failures.

[tautschnig]

I'm afraid that I broke this in diffblue/cbmc@4d4f9e7d182643f8. Fixing PR forthcoming.

[tautschnig]

diffblue/cbmc#6708 addresses this problem.

[tautschnig]

This is now merged in CBMC and will be part of the 5.53.0 release (due to be published 2022-03-17).

[adpaco-aws]

Opened #928 to disable the test since it was failing after CBMC was updated in homebrew. I will revisit this as part of #727 and re-enable the test once 5.53.0 is online.