Feat: {:only} attribute for members
#4075
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
atomb
requested changes
May 24, 2023
| mitigation: "Remove the [{:only}] attribute", | ||
| mitigationIETF: "Must remove the [{:only}] attribute", | ||
| mitigation: "Remove the [{:only}] attribute.", | ||
| mitigationIETF: "Must remove the [{:only}] attribute.", |
There was a problem hiding this comment.
Suggested change
| mitigationIETF: "Must remove the [{:only}] attribute.", | |
| mitigationIETF: "MUST remove the [{:only}] attribute.", |
That's the standard IETF way of writing obligatory requirements.
| public static readonly AssumptionDescription MemberOnly = new( | ||
| issue: "Member has explicit temporary [{:only}] attribute.", | ||
| mitigation: "Remove the [{:only}] attribute.", | ||
| mitigationIETF: "Must remove the [{:only}] attribute.", |
There was a problem hiding this comment.
Suggested change
| mitigationIETF: "Must remove the [{:only}] attribute.", | |
| mitigationIETF: "MUST remove the [{:only}] attribute.", |
Source/DafnyCore/AST/MemberDecls.cs
Outdated
| @@ -105,6 +106,19 @@ public MemberDecl(RangeToken rangeToken, Name name, bool hasStaticKeyword, bool | |||
| } | |||
|
|
|||
| public virtual IEnumerable<Expression> SubExpressions => Enumerable.Empty<Expression>(); | |||
|
|
|||
| public bool HasOnlyAttribute() { | |||
There was a problem hiding this comment.
It's a little unfortunate to have this implemented twice, once on members and once on statements, but it might be worse to lift it up to arbitrary AST nodes, so perhaps it's reasonable to keep it this way.
There was a problem hiding this comment.
Yeah, until we have mix-ins :-)
There was a problem hiding this comment.
Actually with extensions we have mixins. Let me refactor it.
| @@ -3252,6 +3252,14 @@ public XConstraint_EquatableArg(IToken tok, Type a, Type b, bool allowSuperSub, | |||
| currentClass = cl; | |||
| foreach (MemberDecl member in cl.Members) { | |||
| Contract.Assert(VisibleInScope(member)); | |||
| if (Attributes.Find(member.Attributes, "only") is UserSuppliedAttributes attribute) { | |||
| d => d is TopLevelDeclWithMembers memberContainer && | ||
| memberContainer.Members.Any( | ||
| member => | ||
| Attributes.Contains(member.Attributes, "only") |
| @@ -76,4 +76,8 @@ | |||
|
|
|||
| ### Member `AssertOnly` | |||
|
|
|||
| * Assertion has explicit temporary `{:only}` attribute. Must remove the `{:only}` attribute | |||
| * Assertion has explicit temporary `{:only}` attribute. Must remove the `{:only}` attribute. | |||
There was a problem hiding this comment.
Suggested change
| * Assertion has explicit temporary `{:only}` attribute. Must remove the `{:only}` attribute. | |
| * Assertion has explicit temporary `{:only}` attribute. MUST remove the `{:only}` attribute. |
|
|
||
| ### Member `MethodOnly` | ||
|
|
||
| * Member has explicit temporary `{:only}` attribute. Must remove the `{:only}` attribute. |
There was a problem hiding this comment.
Suggested change
| * Member has explicit temporary `{:only}` attribute. Must remove the `{:only}` attribute. | |
| * Member has explicit temporary `{:only}` attribute. MUST remove the `{:only}` attribute. |
docs/dev/news/4074.feat
Outdated
| @@ -0,0 +1 @@ | |||
| `{:only}` attribute for members | |||
There was a problem hiding this comment.
Suggested change
| `{:only}` attribute for members | |
| Allow the `{:only}` attribute to be used on members in addition to `assert` statements |
…com/dafny-lang/dafny into fix-4074-only-on-single-declaration
|
It looks like the merge with |
…com/dafny-lang/dafny into fix-4074-only-on-single-declaration
# Conflicts: # Source/DafnyCore/AST/MemberDecls.cs # Source/DafnyCore/Resolver/ResolutionErrors.cs
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR implements a feature that fixes #4074
I added the corresponding tests, auditor entries and documentations with appropriate links.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.