Programs may perform system calls, which can't be executed during verification.

One good example is HashMaps, which performs a system call to get a random value upon initialization. The program (from #723)

    use std::collections::HashMap;
    #[kani::proof]
    fn harness() {
        let mut map = HashMap::<u32,String>::new();
    }

produces the output

SUMMARY:
 ** 8 of 4964 failed (4956 undetermined)
Failed Checks: Function `std::sys::unix::rand::imp::getrandom::getrandom` with missing definition is unreachable
Failed Checks: Function `syscall` with missing definition is unreachable
Failed Checks: dereference failure: pointer NULL
Failed Checks: dereference failure: pointer invalid
Failed Checks: dereference failure: deallocated dynamic object
Failed Checks: dereference failure: dead object
Failed Checks: dereference failure: pointer outside object bounds
Failed Checks: dereference failure: invalid integer address

Aside from the memory-safety errors, the two "missing function" errors are related to system calls. Two comments:

1. It's not clear to me if both failures are due to the same system call.
2. We need a mechanism around system calls (e.g., stubbing) so we can verify them.

In (1), the problem is around detection and identification. Kani should make clear what system calls were reached, and not report them multiple times if they're the same. The other problem (2) is about how actually verify code including system calls.