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

Creusot panics when using gh! inside a closure #953

Closed
arnaudgolfouse opened this issue Feb 22, 2024 · 4 comments
Closed

Creusot panics when using gh! inside a closure #953

arnaudgolfouse opened this issue Feb 22, 2024 · 4 comments
Labels
bug Something isn't working error-messages Improve error messages

Comments

@arnaudgolfouse
Copy link
Collaborator

This code crashes creusot with "called Option::unwrap() on a None value":

fn f() {
    let x = 1;
    let clos = || {
        let y = gh!(x);
    };
}

It seems this is because creusot assumes a variable captured in gh! is always defined in the enclosing function.

@arnaudgolfouse
Copy link
Collaborator Author

Maybe the following is enough

// creusot/src/translation/specification.rs:125
- Place(p) => p.as_local().unwrap(),
+ Place(p) => p.local,

Am I missing something ?

@jhjourdan
Copy link
Collaborator

Have you tested?

I haven't tested anything, but it seems to me that p should be the closure itself, with the projection being the the captured variable. So no, I would rather bet (but I'm unsure) there is something more subtle to be done here.

@xldenis
Copy link
Collaborator

xldenis commented Feb 22, 2024

Yea it is that line but that's not going to be a correct fix, the purpose of that line is to identify the captures of ghost closures, which need to be erased and I think it glitches out for "ghost captures".

@xldenis xldenis added bug Something isn't working error-messages Improve error messages labels Sep 11, 2024
@arnaudgolfouse
Copy link
Collaborator Author

Fixed by #1106

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working error-messages Improve error messages
Projects
None yet
Development

No branches or pull requests

3 participants