Open Patrick-6 opened 1 year ago
Using any of these 3 pure test_* functions in another function causes an error:
test_*
use prusti_contracts::*; enum Opt<T> { Nil, Some(T) } impl<T> Opt<T> { #[pure] fn test_0(&self) { prusti_assert!(matches!(self, Opt::Nil)); } #[pure] fn test_1(&self) { prusti_assert!(match self {Opt::Nil => true, _ => false}); } #[pure] fn test_2(&self) { prusti_assert!(match self {Opt::Some(_) => true, _ => false}); } } fn bug_trigger(x: Opt<i64>) { x.test_0(); // x.test_1(); // x.test_2(); }
Error:
thread 'rustc' panicked at 'called `Result::unwrap()` on an `Err` value: FailedToObtain(Pred(Field(FieldExpr { base: Field(FieldExpr { base: Field(FieldExpr { base: Local(Local { variable: self: Ref(closure$m_uncategorized_problems$$prusti_panic$$Opt$$$openang$T$closeang$$$test_0$$$opencur$closure$sharp$0$closecur$), position: Position { line: 0, column: 0, id: 0 } }), field: closure_0: Ref(ref$ref$m_uncategorized_problems$$prusti_panic$$Opt$_beg_$__TYPARAM__$_T$0$__$_end_), position: Position { line: 0, column: 0, id: 0 } }), field: val_ref: Ref(ref$m_uncategorized_problems$$prusti_panic$$Opt$_beg_$__TYPARAM__$_T$0$__$_end_), position: Position { line: 0, column: 0, id: 0 } }), field: val_ref: Ref(m_uncategorized_problems$$prusti_panic$$Opt$_beg_$__TYPARAM__$_T$0$__$_end_), position: Position { line: 0, column: 0, id: 0 } }), read))', prusti-viper\src\encoder\snapshot\encoder.rs:1917:10 error: internal compiler error: unexpected panic note: Prusti version: 0.2.1, commit 52cb249 2023-03-23 13:11:26 UTC, built on 2023-03-23 13:22:15 UTC
The error is triggered from here.
Required conditions for this error:
#[pure]
enum Opt
i64
struct TestStruct {}
Manually expanding the matches macro still triggers the error (test_1 and test_2). Matching on either of the enum variants trigger the error.
matches
test_1
test_2
enum
Using any of these 3 pure
test_*
functions in another function causes an error:Error:
The error is triggered from here.
Required conditions for this error:
test_*
must be#[pure]
enum Opt
must be generic; changing it to store an explicit type likei64
orstruct TestStruct {}
will not trigger the errorManually expanding the
matches
macro still triggers the error (test_1
andtest_2
). Matching on either of theenum
variants trigger the error.