I'm trying to test extern_spec for a TryFrom impl. parse_u32 is supposed to prove a cast from a slice to an array. The extern spec currently throws an error internal error: entered unreachable code: External specification declared on a trait implementation did not resolve to a concrete type
I'm trying to test extern_spec for a
TryFrom
impl.parse_u32
is supposed to prove a cast from a slice to an array. The extern spec currently throws an errorinternal error: entered unreachable code: External specification declared on a trait implementation did not resolve to a concrete type
My goal is to specify
try_from
such that the assert-false is not triggered. Currently, prusti fails with an ICEstacktrace
``` thread 'rustc' panicked at prusti-interface/src/specs/external.rs:155:17: internal error: entered unreachable code: External specification declared on a trait implementation did not resolve to a concrete type stack backtrace: 0: 0x792da1362efc - std::backtrace_rs::backtrace::libunwind::trace::h652247f520429b18 at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5 1: 0x792da1362efc - std::backtrace_rs::backtrace::trace_unsynchronized::h20ba733a518048ae at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5 2: 0x792da1362efc - std::sys_common::backtrace::_print_fmt::ha9cb2d71bba5eb16 at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/sys_common/backtrace.rs:67:5 3: 0x792da1362efc -