Failures when iterating over results

[adpaco-aws]

The "Rust by Example" book contains several examples where iterators are used over result values. Take for instance this code (actual example in that section):

// compile-flags: --edition 2018
// rmc-flags: --cbmc-args --unwind 4 --object-bits 9
#![allow(unused)]
pub fn main() {
    let strings = vec!["tofu", "93", "18"];
    let numbers: Vec<_> = strings
        .into_iter()
        .filter_map(|s| s.parse::<i32>().ok())
        .collect();
    println!("Results: {:?}", numbers);
}

This example does not successfully verify with RMC. Running this command

rmc src/test/dashboard/books/Rust\ by\ Example/Error\ handling/Iterating\ over\ Results/22.rs --cbmc-args --unwind 4 --object-bits 9 | grep FAIL

gets me these results:

[std::ptr::const_ptr::<impl *const T>::offset_from.pointer_primitives.12] line 391 pointer outside object bounds in POINTER_OBJECT(var_11): FAILURE
[std::ptr::const_ptr::<impl *const T>::offset_from.pointer_primitives.16] line 391 pointer outside object bounds in POINTER_OBJECT(var_12): FAILURE
[std::result::Result::<T, E>::ok.assertion.1] line 647 unreachable code: FAILURE
VERIFICATION FAILED

But the example runs fine in Rust, producing this output:

Results: [93, 18]

[zhassan-aws]

Kani still reports two spurious failures on this example"

Check 46: _ZN4core3num60_$LT$impl$u20$core..str..traits..FromStr$u20$for$u20$i32$GT$8from_str17h7557cdc4c649c89fE.assertion.1
	 - Status: FAILURE
	 - Description: "assertion false"


Check 64: std::result::Result::<T, E>::ok.assertion.1
	 - Status: FAILURE
	 - Description: "unreachable code"

[celinval]

I think this is a duplicate from #576. These are issues related to the fact that we are not able to link against std functions.

[celinval]

This issue has been resolved by #1785. The issue is covered by the test added in the same PR. https://github.com/model-checking/kani/blob/main/tests/kani/Strings/parse.rs