creusot
creusot copied to clipboard
`custom attribute panicked` on predicate using an `if let` construct
I was trying to work around error[creusot]: called Program function in Logic context "std::result::Result::<T, E>::is_ok"
by defining a predicate like:
#[creusot_contracts::predicate]
pub fn typechecks(e: &Expr) -> bool {
if let Ok(_) = Self::typecheck(e) {
true
} else {
false
}
}
which triggered this error:
error: custom attribute panicked
--> src/lib.rs:124:5
|
124 | #[creusot_contracts::predicate]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= help: message: called `Result::unwrap()` on an `Err` value: Unsupported(#0 bytes(3107..3137), "Let")
Please note that I don't expect this to work since we're still using a "program function in logic context". But a better error message would be much appreciated.
I think the problem here is actually the if let
, which isn't handled in pearlite