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.

Sign up for GitHub

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

Jump to bottom

Make logic VCGen more general, and clarify when it triggers #1238

Open
jhjourdan opened this issue Nov 18, 2024 · 1 comment
Open

Make logic VCGen more general, and clarify when it triggers #1238

jhjourdan opened this issue Nov 18, 2024 · 1 comment
Labels
enhancement New feature or request

Comments

@jhjourdan
Copy link
Collaborator

We need to document when the VCGen used for checking logic declarations (i.e., when there are variant/ensures clauses).

Also the VCGen does not support closures and other pearlite features. We need basic support for this.
@jhjourdan
Copy link
Collaborator Author

Another problem: currently, preconditions of logical functions are not checked when the VCGen does not trigger. This is somewhat clumsy.

@jhjourdan jhjourdan added the enhancement New feature or request label Nov 18, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@jhjourdan