Codegen issue: vtable struct with duplicate components

[nchong-at-aws]

This test requires an additional check in struct_type() of cbmc/goto_program/typ.rs to ensure that the struct's components are unique. In this case, the vtable contains two foo fn pointers.

trait A {
    fn foo(&self) -> i32;
}

trait B {
    fn foo(&self) -> i32;
}

trait T : A + B {
}

struct S {
    x : i32,
    y : i32,
}

impl S {
    fn new(a:i32, b:i32) -> S {
        S {x:a, y:b}
    }
    fn new_box(a:i32, b:i32) -> Box<dyn T> { 
        Box::new(S::new(a,b))
    }
}


impl A for S {
    fn foo(&self) -> i32{
        self.x
    }
}

impl B for S {
    fn foo(&self) -> i32{
        self.y
    }
}

impl T for S {
}

fn main() {
    let t = S::new_box(1,2);
    let a = <dyn T as A>::foo(&*t);
    assert!(a == 1);
    let b = <dyn T as B>::foo(&*t);
    assert!(b == 2);
}

[adpaco]

#68 is a temporary workaround.

We have the unsupported test written above in:

rust-tests/cbmc-reg/DynTrait/vtable_duplicate_fields_fixme.rs