Fix: @VerifyOnly now working as expected

Source/DafnyCore/AST/Attributes.cs

@@ -53,12 +53,12 @@ void ObjectInvariant() {
     Contract.Invariant(cce.NonNullElements(Args));
   }
 
-  public static string AxiomAttributeName = "axiom";
-  public static string ConcurrentAttributeName = "concurrent";
-  public static string AssumeConcurrentAttributeName = "assume_concurrent";
-  public static string ExternAttributeName = "extern";
-  public static string VerifyAttributeName = "verify";
-  public static string AutoGeneratedAttributeName = "auto_generated";
+  public static readonly string AxiomAttributeName = "axiom";
+  public static readonly string ConcurrentAttributeName = "concurrent";
+  public static readonly string AssumeConcurrentAttributeName = "assume_concurrent";
+  public static readonly string ExternAttributeName = "extern";
+  public static readonly string VerifyAttributeName = "verify";
+  public static readonly string AutoGeneratedAttributeName = "auto_generated";
 
   public string Name;
   /*Frozen*/
@@ -287,18 +287,18 @@ static BuiltInAtAttributeSyntax BuiltIn(string name) {
   }
 
   // Helper to create an old-style attribute
-  private static Attributes A(string name, params Expression[] args) {
-    return new Attributes(name, args.Select(arg =>
+  private static Attributes A(IOrigin origin, string name, params Expression[] args) {
+    return new Attributes(origin, name, args.Select(arg =>
       arg is DefaultValueExpression defaultExpr ? defaultExpr.Resolved : arg).ToList(), null);
   }
 
   // Helper to create an old-style attribute with only one argument
-  private static Attributes A1(string name, ActualBindings bindings) {
+  private static Attributes A1(IOrigin origin, string name, ActualBindings bindings) {
     if (Get(bindings, 0, out var expr) && expr != null) {
-      return A(name, expr);
+      return A(origin, name, expr);
     }
 
-    return A(name);
+    return A(origin, name);
   }
 
   // Given a user-supplied @-attribute, expand it if recognized as builtin to an old-style attribute
@@ -333,145 +333,146 @@ private static Attributes A1(string name, ActualBindings bindings) {
     var intDecl = resolver.SystemModuleManager.valuetypeDecls.First(valueTypeDecl => valueTypeDecl.Name == PreType.TypeNameInt);
 
     atAttribute.Arg.PreType = new DPreType(intDecl, []);
+    var tok = atAttribute.Origin;
 
     switch (name) {
       case "AssumeCrossModuleTermination": {
-          return A("AssumeCrossModuleTermination");
+          return A(tok, "AssumeCrossModuleTermination");
         }
       case "AutoContracts": {
-          return A("autocontracts");
+          return A(tok, "autocontracts");
         }
       case "AutoRequires": {
-          return A("autoReq");
+          return A(tok, "autoReq");
         }
       case "AutoRevealDependenciesAll": {
-          return A1("autoRevealDependencies", bindings);
+          return A1(tok, "autoRevealDependencies", bindings);
         }
       case "AutoRevealDependencies": {
-          return A1("autoRevealDependencies", bindings);
+          return A1(tok, "autoRevealDependencies", bindings);
         }
       case "Axiom": {
-          return A(AxiomAttributeName);
+          return A(tok, AxiomAttributeName);
         }
       case "Compile": {
-          return A1("compile", bindings);
+          return A1(tok, "compile", bindings);
         }
       case "Concurrent": {
-          return A(ConcurrentAttributeName);
+          return A(tok, ConcurrentAttributeName);
         }
       case "DisableNonlinearArithmetic": {
-          return A1("disableNonlinearArithmetic", bindings);
+          return A1(tok, "disableNonlinearArithmetic", bindings);
         }
       case "Fuel": {
           if (Get(bindings, 0, out var lowFuel) && lowFuel != null) {
             if (Get(bindings, 1, out var highFuel) && highFuel != null) {
               if (Get(bindings, 2, out var functionName) && IsStringNotEmpty(functionName)) {
-                return A("fuel", functionName!, lowFuel, highFuel);
+                return A(tok, "fuel", functionName!, lowFuel, highFuel);
               }
 
-              return A("fuel", lowFuel, highFuel);
+              return A(tok, "fuel", lowFuel, highFuel);
             }
 
-            return A("fuel", lowFuel);
+            return A(tok, "fuel", lowFuel);
           }
 
-          return A("fuel");
+          return A(tok, "fuel");
         }
       case "IsolateAssertions": {
-          return A("isolate_assertions");
+          return A(tok, "isolate_assertions");
         }
       case "NativeUInt8": {
-          return A("nativeType", DefaultString("byte"));
+          return A(tok, "nativeType", DefaultString("byte"));
         }
       case "NativeInt8": {
-          return A("nativeType", DefaultString("sbyte"));
+          return A(tok, "nativeType", DefaultString("sbyte"));
         }
       case "NativeUInt16": {
-          return A("nativeType", DefaultString("ushort"));
+          return A(tok, "nativeType", DefaultString("ushort"));
         }
       case "NativeInt16": {
-          return A("nativeType", DefaultString("short"));
+          return A(tok, "nativeType", DefaultString("short"));
         }
       case "NativeUInt32": {
-          return A("nativeType", DefaultString("uint"));
+          return A(tok, "nativeType", DefaultString("uint"));
         }
       case "NativeInt32": {
-          return A("nativeType", DefaultString("int"));
+          return A(tok, "nativeType", DefaultString("int"));
         }
       case "NativeInt53": {
-          return A("nativeType", DefaultString("number"));
+          return A(tok, "nativeType", DefaultString("number"));
         }
       case "NativeUInt64": {
-          return A("nativeType", DefaultString("ulong"));
+          return A(tok, "nativeType", DefaultString("ulong"));
         }
       case "NativeInt64": {
-          return A("nativeType", DefaultString("long"));
+          return A(tok, "nativeType", DefaultString("long"));
         }
       case "NativeUInt128": {
-          return A("nativeType", DefaultString("udoublelong"));
+          return A(tok, "nativeType", DefaultString("udoublelong"));
         }
       case "NativeInt128": {
-          return A("nativeType", DefaultString("doublelong"));
+          return A(tok, "nativeType", DefaultString("doublelong"));
         }
       case "NativeInt": {
-          return A("nativeType", DefaultBool(true));
+          return A(tok, "nativeType", DefaultBool(true));
         }
       case "NativeNone": {
-          return A("nativeType", DefaultBool(false));
+          return A(tok, "nativeType", DefaultBool(false));
         }
       case "NativeIntOrReal": {
-          return A("nativeType");
+          return A(tok, "nativeType");
         }
       case "Options": {
-          return A1("options", bindings);
+          return A1(tok, "options", bindings);
         }
       case "Print": {
-          return A("print");
+          return A(tok, "print");
         }
       case "Priority": {
-          return A1("priority", bindings);
+          return A1(tok, "priority", bindings);
         }
       case "ResourceLimit": {
-          return A1("resource_limit", bindings);
+          return A1(tok, "resource_limit", bindings);
         }
       case "Synthesize": {
-          return A("synthesize");
+          return A(tok, "synthesize");
         }
       case "TimeLimit": {
-          return A1("timeLimit", bindings);
+          return A1(tok, "timeLimit", bindings);
         }
       case "TimeLimitMultiplier": {
-          return A1("timeLimitMultiplier", bindings);
+          return A1(tok, "timeLimitMultiplier", bindings);
         }
       case "TailRecursion": {
-          return A("tailrecursion");
+          return A(tok, "tailrecursion");
         }
       case "Test": {
-          return A("test");
+          return A(tok, "test");
         }
       case "TestEntry": {
-          return A("TestEntry");
+          return A(tok, "TestEntry");
         }
       case "TestInline": {
-          return A1("testInline", bindings);
+          return A1(tok, "testInline", bindings);
         }
       case "Transparent": {
-          return A("transparent");
+          return A(tok, "transparent");
         }
       case "VcsMaxCost": {
-          return A1("vcs_max_cost", bindings);
+          return A1(tok, "vcs_max_cost", bindings);
         }
       case "VcsMaxKeepGoingSplits": {
-          return A1("vcs_max_keep_going_splits", bindings);
+          return A1(tok, "vcs_max_keep_going_splits", bindings);
         }
       case "VcsMaxSplits": {
-          return A1("vcs_max_splits", bindings);
+          return A1(tok, "vcs_max_splits", bindings);
         }
       case "Verify": {
-          return A1(VerifyAttributeName, bindings);
+          return A1(tok, VerifyAttributeName, bindings);
         }
       case "VerifyOnly": {
-          return A("only");
+          return A(tok, "only");
         }
       default: {
           throw new Exception("@-Attribute added to Attributes.BuiltinAtAttributes needs to be handled here");
@@ -684,7 +685,7 @@ public static bool TryGetBuiltinAtAttribute(string name, out BuiltInAtAttributeS
 
   // Overridable method to clone the attribute as if the new attribute was placed after "prev" in the source code
   public virtual Attributes CloneAfter(Attributes? prev) {
-    return new Attributes(Name, Args, prev);
+    return new Attributes(Origin, Name, Args, prev);
   }
 
   //////// Helpers for parsing attributes //////////////////
@@ -756,7 +757,7 @@ public UserSuppliedAtAttribute(IOrigin origin, Expression arg, Attributes? prev)
   public Expression Arg => Args[0];
 
   public override Attributes CloneAfter(Attributes? prev) {
-    return new UserSuppliedAtAttribute(AtSign, Args[0], prev);
+    return new UserSuppliedAtAttribute(Origin, Args[0], prev);
   }
 
   // Name of this @-Attribute, which is the part right after the @

Source/DafnyCore/AST/Members/MemberDecl.cs

@@ -115,7 +115,7 @@ public override IEnumerable<Assumption> Assumptions(Declaration decl) {
     foreach (var a in base.Assumptions(this)) {
       yield return a;
     }
-    if (this.HasUserAttribute("only", out _)) {
+    if (Attributes.Find(this.Attributes, "only") != null) {
       yield return new Assumption(decl, Origin, AssumptionDescription.MemberOnly);
     }
   }

Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs

@@ -68,7 +68,7 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext co
       }
     }
 
-    if (this.HasUserAttribute("only", out var attribute)) {
+    if (Attributes.Find(Attributes, "only") is { } attribute) {
       resolver.Reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_assert_only_assumes_others.ToString(), attribute!.Origin,
         "Assertion with {:only} temporarily transforms other assertions into assumptions");
       if (attribute.Args.Count >= 1

Source/DafnyCore/Auditor/Assumption.cs

@@ -105,9 +105,9 @@ public static AssumptionDescription NoBody(bool isGhost) {
   );
 
   public static readonly AssumptionDescription MemberOnly = new(
-    Issue: "Member has explicit temporary [{:only}] attribute.",
-    Mitigation: "Remove the [{:only}] attribute.",
-    MitigationIetf: "MUST remove the [{:only}] attribute.",
+    Issue: "Member has explicit temporary [@VerifyOnly] attribute.",
+    Mitigation: "Remove the [@VerifyOnly] attribute.",
+    MitigationIetf: "MUST remove the [@VerifyOnly] attribute.",
     IsExplicit: true
   );
 }

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -1493,12 +1493,12 @@ public void ResolveTopLevelDecls_Core(List<TopLevelDecl> declarations,
       }
 
       foreach (var member in declarations.OfType<TopLevelDeclWithMembers>().SelectMany(d => d.Members)) {
-        if (member.HasUserAttribute("only", out var attribute)) {
+        if (Attributes.Find(member.Attributes, "only") is { } attribute) {
           reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_member_only_assumes_other.ToString(), attribute.Origin,
-            "Members with {:only} temporarily disable the verification of other members in the entire file");
+            "Members with @VerifyOnly temporarily disable the verification of other members in the entire file");
           if (attribute.Args.Count >= 1) {
             reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_member_only_has_no_before_after.ToString(), attribute.Args[0].Origin,
-              "{:only} on members does not support arguments");
+              "@VerifyOnly on members does not support arguments");
           }
         }
       }

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -2791,12 +2791,12 @@ void ResolveClassMemberBodies(TopLevelDeclWithMembers cl) {
       currentClass = cl;
       foreach (MemberDecl member in cl.Members) {
         Contract.Assert(VisibleInScope(member));
-        if (member.HasUserAttribute("only", out var attribute)) {
+        if (Attributes.Find(member.Attributes, "only") is { } attribute) {
           reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_member_only_assumes_other.ToString(), attribute.Origin,
-            "Members with {:only} temporarily disable the verification of other members in the entire file");
+            "Members with @VerifyOnly temporarily disable the verification of other members in the entire file");
           if (attribute.Args.Count >= 1) {
             reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_member_only_has_no_before_after.ToString(), attribute.Args[0].Origin,
-              "{:only} on members does not support arguments");
+              "@VerifyOnly on members does not support arguments");
           }
         }
         if (member is Field) {

Source/DafnyCore/Resolver/ResolutionErrors.cs

@@ -105,13 +105,13 @@ This warning is a reminder about it.
 ", Replace("before", "Replace with \"before\""));
     Add(ErrorId.r_member_only_assumes_other,
       @"
-When annotating a member with the `{:only}` attribute, all other members of any declaration in the same file are not verified.
+When annotating a member with the `@VerifyOnly` attribute, all other members of any declaration in the same file are not verified.
 This is a good way to focus on a method, a function or a lemma and its proof, but this annotation has to be removed once finished.
 This warning is a reminder about it.
-", Remove(true, "Finish focusing and remove {:only}"));
+", Remove(true, "Finish focusing and remove @VerifyOnly"));
     Add(ErrorId.r_member_only_has_no_before_after,
         @"
-The `{:only}` attribute on members does not accept optional argument like ""after"" or ""before"" like the `{:only}` attribute on assertions can.
+The `@VerifyOnly` attribute on members does not accept optional argument like ""after"" or ""before"" like the `{:only}` attribute on assertions can.
 ",
         Remove(true, "Remove this unused argument"));
   }

Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs

@@ -45,7 +45,7 @@ void AddClassMembers(TopLevelDeclWithMembers c, bool includeAllMethods, bool inc
         CurrentDeclaration = member;
         var ignored =
           filesWhereOnlyMembersAreVerified.Contains(member.Origin.Uri) &&
-          !member.HasUserAttribute("only", out _);
+          Attributes.Find(member.Attributes, "only") is null;
         if (ignored) {
           assertionOnlyFilter = _ => false;
         } else {

Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs

@@ -29,7 +29,7 @@ await VerifyTrace(@"
  ? :method NotVerified() { // Should not be highlighted in green
  ? :  assert 1 == 0;
  ? :}
- | :method {:only} Verified() { // Verified
+ | :@VerifyOnly method Verified() { // Verified
  | :  assert true;
  | :}
  ? :method NotVerified2() { // Should not be highlighted in green

Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy

@@ -94,7 +94,6 @@ method Test(a: int, b: int, c: int)
   assert c > a;
 }
 
-@VerifyOnly
 @Print
 @Priority(2)
 @ResourceLimit("1000")

Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy

@@ -151,7 +151,7 @@ method AssertOnly() {
   assert false;
 }
 
-method {:only} MethodOnly() {
+@VerifyOnly method MethodOnly() {
   assert false;
 }
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy-ietf.md.expect

@@ -85,7 +85,7 @@
 
 ### Member `MethodOnly`
 
-* Member has explicit temporary `{:only}` attribute. MUST remove the `{:only}` attribute.
+* Member has explicit temporary `@VerifyOnly` attribute. MUST remove the `@VerifyOnly` attribute.
 
 ### Member `GenerateBytesWithAxiom`
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.expect

@@ -6,7 +6,7 @@ TestAuditor.dfy(95,4): Warning: this forall statement has no body
 TestAuditor.dfy(102,4): Warning: this loop has no body (loop frame: i)
 TestAuditor.dfy(139,2): Warning: this forall statement has no body
 TestAuditor.dfy(143,2): Warning: this loop has no body (loop frame: i)
-TestAuditor.dfy(154,9): Warning: Members with {:only} temporarily disable the verification of other members in the entire file
+TestAuditor.dfy(154,0): Warning: Members with @VerifyOnly temporarily disable the verification of other members in the entire file
 TestAuditor.dfy(93,10): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section on quantifier instantiation rules in the reference manual.
 TestAuditor.dfy(95,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section on quantifier instantiation rules in the reference manual.
 TestAuditor.dfy(139,2): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section on quantifier instantiation rules in the reference manual.
@@ -30,7 +30,7 @@ TestAuditor.dfy(128,27): Warning: AssumedConcurrentMethod: Reads clause has `{:a
 TestAuditor.dfy(128,27): Warning: AssumedConcurrentMethod: Modifies clause has `{:assume_concurrent}` attribute. Possible mitigation: Manually review and test in a concurrent setting.
 TestAuditor.dfy(135,16): Warning: AxiomWithStuffInIt: Declaration has explicit `{:axiom}` attribute. Possible mitigation: Provide a proof or test.
 TestAuditor.dfy(150,2): Warning: AssertOnly: Assertion has explicit temporary `{:only}` attribute. Possible mitigation: Remove the `{:only}` attribute.
-TestAuditor.dfy(154,15): Warning: MethodOnly: Member has explicit temporary `{:only}` attribute. Possible mitigation: Remove the `{:only}` attribute.
+TestAuditor.dfy(154,19): Warning: MethodOnly: Member has explicit temporary `@VerifyOnly` attribute. Possible mitigation: Remove the `@VerifyOnly` attribute.
 TestAuditor.dfy(160,26): Warning: GenerateBytesWithAxiom: Declaration has explicit `{:axiom}` attribute. Possible mitigation: Provide a proof or test.
 TestAuditor.dfy(164,28): Warning: ExternFunctionWithAxiom: Declaration has explicit `{:axiom}` attribute. Possible mitigation: Provide a proof or test.
 TestAuditor.dfy(89,27): Warning: T: Trait method calls may not terminate (uses `{:termination false}`). Possible mitigation: Remove if possible.