creusot icon indicating copy to clipboard operation
creusot copied to clipboard

`custom attribute panicked` on predicate using an `if let` construct

Open adpaco-aws opened this issue 1 year ago • 1 comments

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.

adpaco-aws avatar Nov 13 '23 21:11 adpaco-aws

I think the problem here is actually the if let, which isn't handled in pearlite

xldenis avatar Nov 13 '23 22:11 xldenis