Open nishanthkarthik opened 3 months ago
I am using Prusti version: 0.2.2, commit 528f4c2 2024-03-06 10:13:12 UTC, built on 2024-03-06 10:25:48 UTC
Prusti version: 0.2.2, commit 528f4c2 2024-03-06 10:13:12 UTC, built on 2024-03-06 10:25:48 UTC
use prusti_contracts::*; struct Token<T> { _p: std::marker::PhantomData<T> } #[model] struct Token<#[generic] T: Copy> { ptrs: Seq<*mut T>, }
This panics with a not-implemented. I followed the example from the examples in prusti-tests using a model with a built-in seq.
@Aurel300
I am using
Prusti version: 0.2.2, commit 528f4c2 2024-03-06 10:13:12 UTC, built on 2024-03-06 10:25:48 UTC
This panics with a not-implemented. I followed the example from the examples in prusti-tests using a model with a built-in seq.
backtrace
``` thread 'rustc' panicked at prusti-viper/src/encoder/high/lower/predicates.rs:36:55: not implemented stack backtrace: 0: 0x717ce1562efc - std::backtrace_rs::backtrace::libunwind::trace::h652247f520429b18 at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5 1: 0x717ce1562efc - std::backtrace_rs::backtrace::trace_unsynchronized::h20ba733a518048ae at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5 2: 0x717ce1562efc - std::sys_common::backtrace::_print_fmt::ha9cb2d71bba5eb16 at /rustc/ca2b74f1ae5075d62e223c0a91574a1fc3f51c7c/library/std/src/sys_common/backtrace.rs:67:5 3: 0x717ce1562efc -