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

Fix incorrect parsing of string contains "verus!{". #72

Merged
merged 5 commits into from
Jun 1, 2024

Conversation

XuhengLi
Copy link
Contributor

non_verus is defined to accept ANY which might be of low precedency. When a string literal in non_verus contains "verus!{", VerusParser fails to parse the string and throws an error indicating the string is parsed into verus_macro_use.

This patch modfies non_verus so it accepts string, raw_string, etc., explicitly so string literals with "verus!{" can be correctly parsed.

verus-minimal is changed as well otherwise rustfmt shipped in this crate cannot format the non-verus code correctly.

A companion unit test which should fail without this patch is included.

non_verus is defined to accept ANY which might be of low precedency.
When a string literal in non_verus contains "verus!{", VerusParser fails to parse the string and throws an error indicating the string is parsed into verus_macro_use.

This patch modfies non_verus so it accepts string, raw_string, etc., explicitly so string literals with "verus!{" can be correctly parsed.

verus-minimal is changed as well otherwise rustfmt shipped in this crate cannot format the non-verus code correctly.

A companion unit test which should fail without this patch is included.
@jaybosamiya jaybosamiya self-requested a review May 29, 2024 22:13
Copy link
Collaborator

@jaybosamiya jaybosamiya left a comment

Choose a reason for hiding this comment

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

Awesome, thanks for fixing this issue!

This overall looks good to me, modulo the minor comment about the comment which would be nice to add in before we merge this.

Majority of the addition to verus-minimal.pest is copying over string,...ray_byte_string into it; just thinking about longer term maintainability (as a TODO item for myself to take care of after this PR; no changes needed here) is to add some comments on which things need to stay in sync.

src/verus.pest Outdated Show resolved Hide resolved
@XuhengLi
Copy link
Contributor Author

Formatting updates.

@jaybosamiya
Copy link
Collaborator

jaybosamiya commented Jun 1, 2024

Overall, looks good to me. Thanks for your first contribution to verusfmt! Will merge it in once CI goes green. (Edit: I can't squash merge from my phone; will merge once I get to my laptop)

@jaybosamiya jaybosamiya merged commit 4a450c5 into verus-lang:main Jun 1, 2024
7 checks passed
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

Successfully merging this pull request may close these issues.

2 participants