Incorrect verification success on print statement

[avanhatt]

RMC run with bound checking says verification is successful on this function, which actually seg faults.

Command: rmc --keep-temps --gen-c src/test/cbmc/DynTrait/fixme_offset.rs --pointer-check --bounds-check

// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
// SPDX-License-Identifier: Apache-2.0 OR MIT

struct Foo {}
trait Trait {
    fn func(&self) -> i32;
}

impl Trait for Foo {
    fn func(&self) -> i32 {
        1 as i32
    }
}

fn foo() -> Box<dyn Trait> {
    Box::new(Foo {}) 
}

fn main() {
    let f = foo();
    unsafe {
        let f_ptr = Box::into_raw(f) as *const usize;
        println!("{}", *(f_ptr.offset(100000)));
    }
}

RMC result:

/Users/avanhatt/research/rmc/src/test/cbmc/DynTrait/fixme_offset.rs function main
[main.assertion.3] line 20 resume instruction: SUCCESS
[main.assertion.1] line 22 Non-null virtual function call for "::Trait::func": SUCCESS
[main.pointer_dereference.1] line 22 dereference failure: pointer NULL in var_3.vtable->::Trait::func: SUCCESS
[main.pointer_dereference.2] line 22 dereference failure: pointer invalid in var_3.vtable->::Trait::func: SUCCESS
[main.pointer_dereference.3] line 22 dereference failure: deallocated dynamic object in var_3.vtable->::Trait::func: SUCCESS
[main.pointer_dereference.4] line 22 dereference failure: dead object in var_3.vtable->::Trait::func: SUCCESS
[main.pointer_dereference.5] line 22 dereference failure: pointer outside object bounds in var_3.vtable->::Trait::func: SUCCESS
[main.pointer_dereference.6] line 22 dereference failure: invalid integer address in var_3.vtable->::Trait::func: SUCCESS
[main.assertion.2] line 23 assertion failed: x == 1: SUCCESS

<builtin-library-malloc> function malloc
[malloc.assertion.1] line 26 max allocation size exceeded: SUCCESS
[malloc.assertion.2] line 31 max allocation may fail: SUCCESS

** 0 of 78 failed (1 iterations)
VERIFICATION SUCCESSFUL

Rust result:

timeout: the monitored command dumped core
/playground/tools/entrypoint.sh: line 11:     9 Segmentation fault      timeout --signal=KILL ${timeout} "$@"

[avanhatt]

Looks like this is a slightly different issue: if you change the dereference to this, it fails as expected:

let bad = *(f_ptr.offset(100000));