Skip to content

Fixing invalid Boogie code for quantified predicates without parameters#541

Merged
marcoeilers merged 2 commits into
masterfrom
meilers_fix_391
Dec 30, 2024
Merged

Fixing invalid Boogie code for quantified predicates without parameters#541
marcoeilers merged 2 commits into
masterfrom
meilers_fix_391

Conversation

@marcoeilers

@marcoeilers marcoeilers commented Dec 28, 2024

Copy link
Copy Markdown
Contributor

Fixing #391, though we currently do not get the error described there.
For this program:

predicate p()

method m()
  ensures forall i: Int :: p()

we currently get an error from Boogie because Carbon outputs a quantifier with no quantified variables.

viper-admin
viper-admin approved these changes Dec 30, 2024
View reviewed changes

@viper-admin viper-admin left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@marcoeilers marcoeilers merged commit b7b5950 into master Dec 30, 2024
@marcoeilers marcoeilers deleted the meilers_fix_391 branch December 30, 2024 14:54
This was referenced Dec 30, 2024
Merged
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@viper-admin viper-admin viper-admin approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@marcoeilers @viper-admin
⚡