High offsets cause wrapping-around behavior in CBMC

[adpaco-aws]

In an example introduced in #1131 , we reproduced an issue where a high offset causes a "wrapping around" behavior in CBMC.
There is more information on the test, but basically we should either enforce stricter checks than Rust (because of CBMC object bits limitations) or add these checks to CBMC itself.

[celinval]

I think we will need to stop using CBMC's pointer offset operation in the case of wrapping_offset. Instead, we need to convert the pointer into a usize, perform a wrapping_add considering the object size, then convert back to a pointer.

[celinval]

BTW, here is a small example that shows the problem:

/// This harness shows the issue with the current implementation of wrapping offset.
///
/// Invoking `wrapping_byte_offset` should return a pointer that is different from the original
/// pointer if the offset value is not 0.
#[kani::proof]
fn fixme_incorrect_wrapping_offset() {
    let ptr: *const u8 = &0u8;
    let offset = kani::any_where(|v: &isize| *v != 0);
    let new_ptr = ptr.wrapping_byte_offset(offset);
    assert_ne!(ptr, new_ptr, "Expected new_ptr to be different than ptr");
}