Rustc's type checking guarantees that any copy(..) in LLBC applies to a type that has the Copy bound. Because copy(..) means "copying just the bits", there is no need to find the corresponding Copy implementation either, so https://github.com/AeneasVerif/charon/pull/111 makes ty_is_copyable always return true.
Rustc's type checking guarantees that any
copy(..)in LLBC applies to a type that has theCopybound. Becausecopy(..)means "copying just the bits", there is no need to find the correspondingCopyimplementation either, so https://github.com/AeneasVerif/charon/pull/111 makesty_is_copyablealways returntrue.This bumps charon to https://github.com/AeneasVerif/charon/pull/111.
Fixes https://github.com/AeneasVerif/aeneas/issues/118