Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Panic when selecting a trigger that involves a closure argument #946

Open
matthias-brun opened this issue Dec 22, 2023 · 0 comments
Open

Comments

@matthias-brun
Copy link
Collaborator

I don't know if such a trigger would even be reasonable but Verus probably shouldn't panic.

use vstd::prelude::*;

verus!{

fn main() { }

proof fn x()
    ensures forall|P: FnSpec(nat) -> bool| Set::new(|i: nat| false && #[trigger] P(i)).finite(),
{}
}
ξ verus-release /st/verus/test.rs
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:506:17:
internal error: ill-typed AIR code: error 'use of undeclared variable i~29$' in expression 'i~29$'
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:332:17:
dropped, expected call to `into_inner` instead
stack backtrace:
[ ... backtrace omitted ... ]
thread '<unnamed>' panicked at library/core/src/panicking.rs:126:5:
panic in a function that cannot unwind
stack backtrace:
[ ... backtrace omitted ... ]
thread caused non-unwinding panic. aborting.
zsh: abort (core dumped)  /st/verus/verus/source/target-verus/release/verus /st/verus/test.rs
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant