Dyn traits are unimplemented

[the-ssd]

Hello, I was trying to use creusot to verify the redox kernel didn't have any panics, and ran into a bit of a problem.

The kernel uses "dyn traits".

This is where creusot crashes

Is it possible to implement them?

Here is a maybe working implementation

ImplSource::Builtin(_, _) => match *substs.type_at(0).kind() {
    rustc_middle::ty::Closure(closure_def_id, closure_substs) => {
        TraitResolved::Instance(closure_def_id, closure_substs)
    }
    rustc_middle::ty::Dynamic(_, _, _) => {
        TraitResolved::UnknownNotFound
    }
    _ => {
        todo!()
    }
},

If it is resolved, then I still have a problem with error: const generic parameters are not yet supported, but it compiles on stable and nightly

pub struct AlignedBox<T: ?Sized, const ALIGN: usize> {
    inner: Unique<T>,
}

impl<T: ?Sized, const ALIGN: usize> AlignedBox<T, ALIGN> {
    fn layout(&self) -> Layout {
        layout_upgrade_align(Layout::for_value::<T>(&*self), ALIGN) // error: const generic parameters are not yet supported
    }
}
const fn layout_upgrade_align(layout: Layout, align: usize) -> Layout {
    const fn max(a: usize, b: usize) -> usize {
        if a > b {
            a
        } else {
            b
        }
    }
    let Ok(x) = Layout::from_size_align(layout.size(), max(align, layout.align())) else {
        panic!("failed to calculate layout");
    };
    x
}

[the-ssd]

moved to an issue #1284