Investigate failed check in memcmp #1489
Description
This was discovered in #1332, but also occurs in a synchronous context:
#[kani::proof]
pub fn main() {
let coll: Result<Vec<u32>, ()> = std::iter::empty().collect();
assert_eq!(Ok(vec![]), coll);
}Running this with Kani gives the result:
SUMMARY:
** 2 of 436 failed
Failed Checks: memcmp region 1 readable
File: "<builtin-library-memcmp>", line 19, in memcmp
Failed Checks: memcpy region 2 readable
File: "<builtin-library-memcmp>", line 21, in memcmp
VERIFICATION:- FAILED
Metadata
Metadata
Assignees
Labels
No labels