Closed
Description
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]
Activity