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

Escherichia/opaque #227

Merged
merged 25 commits into from
Jun 6, 2024
Merged

Escherichia/opaque #227

merged 25 commits into from
Jun 6, 2024

Conversation

EschericHya
Copy link
Contributor

@EschericHya EschericHya commented Jun 4, 2024 •
edited
Loading

Fixes #206

Escherichia added 13 commits May 29, 2024 11:29
sonmarcho
sonmarcho requested changes Jun 4, 2024
View reviewed changes
@sonmarcho
Copy link
Member

I'm asking for a few modifications, but overall it works.

@Nadrieril
Copy link
Member

Could you add a test for all the new cases you cover? That means adding charon/tests/ui/opaque_attribute.rs that contains a few cases like the atribute on a function, on a trait etc to record the output.

sonmarcho
sonmarcho requested changes Jun 6, 2024
View reviewed changes
Copy link
Member

@sonmarcho sonmarcho left a comment

Choose a reason for hiding this comment

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

Still some nitpicks, but the modifications should be super quick to to.
And, yes, we should add some tests.

@Nadrieril
Copy link
Member

Hm, something is weird: the changes to charon-ml are missing but the CI is passing 🤔

@Nadrieril
Copy link
Member

Oh sorry we skip serializing the field so there's no charon-ml change to do.

@Nadrieril Nadrieril mentioned this pull request Jun 6, 2024
Closed
@sonmarcho sonmarcho merged commit 65e64bd into main Jun 6, 2024
10 checks passed
@sonmarcho sonmarcho deleted the escherichia/opaque branch June 6, 2024 14:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Nadrieril Nadrieril Nadrieril left review comments

@sonmarcho sonmarcho sonmarcho requested changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Add an attribute to mark definitions as opaque
3 participants
@EschericHya @sonmarcho @Nadrieril