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

[Feature request]: Warn about unrecognized attributes #3128

Open
atomb opened this issue Nov 29, 2022 · 2 comments
Open

[Feature request]: Warn about unrecognized attributes #3128

atomb opened this issue Nov 29, 2022 · 2 comments
Labels
difficulty: easy Issues that should take a few days at most to fix difficulty: good-first-issue Good first issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking

Comments

@atomb
Copy link
Member

atomb commented Nov 29, 2022

What is the feature you would like to see in a future version of Dafny?

Currently, Dafny accepts any {:attribute} markers present in the source code, whether it recognizes attribute or not. It would be nice to, at least optionally, warn about any attribute that Dafny doesn't know about, to guard against misspelling.
@atomb atomb added kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking difficulty: easy Issues that should take a few days at most to fix labels Nov 29, 2022
@alex-chew
Copy link
Contributor

I'd like for this mechanism to be made extensible, so that (for example) a compiler plugin may define a custom attribute, and Dafny will not emit an "unrecognized attribute" warning on usages of that custom attribute.

@MikaelMayer MikaelMayer added the difficulty: good-first-issue Good first issues label Nov 30, 2022
@robin-aws
Copy link
Member

My proposal in #3149 seems to address both points AFACIT, let me know what you think!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
difficulty: easy Issues that should take a few days at most to fix difficulty: good-first-issue Good first issues kind: enhancement Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny part: resolver Resolution and typechecking
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@atomb @MikaelMayer @alex-chew @robin-aws