diff --git a/Source/DafnyCore/AST/Attributes.cs b/Source/DafnyCore/AST/Attributes.cs index 79ecb1f6ece..c5504b29820 100644 --- a/Source/DafnyCore/AST/Attributes.cs +++ b/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 @ diff --git a/Source/DafnyCore/AST/Members/MemberDecl.cs b/Source/DafnyCore/AST/Members/MemberDecl.cs index 9d0a4262773..42c48562e0f 100644 --- a/Source/DafnyCore/AST/Members/MemberDecl.cs +++ b/Source/DafnyCore/AST/Members/MemberDecl.cs @@ -115,7 +115,7 @@ public override IEnumerable 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); } } diff --git a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs b/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs index cd2bb83f84f..7878e510a6d 100644 --- a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs +++ b/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 diff --git a/Source/DafnyCore/Auditor/Assumption.cs b/Source/DafnyCore/Auditor/Assumption.cs index 9398112eae6..aec293c36d3 100644 --- a/Source/DafnyCore/Auditor/Assumption.cs +++ b/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 ); } diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 03562d05e5d..36d812e55ff 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -1493,12 +1493,12 @@ public void ResolveTopLevelDecls_Core(List declarations, } foreach (var member in declarations.OfType().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"); } } } diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index ab799a3db26..61f5309c597 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/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) { diff --git a/Source/DafnyCore/Resolver/ResolutionErrors.cs b/Source/DafnyCore/Resolver/ResolutionErrors.cs index 084a2136259..bd448c5f246 100644 --- a/Source/DafnyCore/Resolver/ResolutionErrors.cs +++ b/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")); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index 2b3164ab835..c69b3a6aeb0 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/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 { diff --git a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs b/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs index c4e8bfd100d..2d3ceb085a9 100644 --- a/Source/DafnyLanguageServer.Test/GutterStatus/SimpleLinearVerificationGutterStatusTester.cs +++ b/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 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy index 4179a4508c5..c5eef8df749 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/at-attributes/at-attributes-acceptable-builtin.dfy +++ b/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") diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy index 6983db632a2..f0377651286 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy @@ -151,7 +151,7 @@ method AssertOnly() { assert false; } -method {:only} MethodOnly() { +@VerifyOnly method MethodOnly() { assert false; } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy-ietf.md.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy-ietf.md.expect index 9ee3b2ebdd6..4a7e0712bc7 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy-ietf.md.expect +++ b/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` diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.expect index 14af8b728e5..d9d6622aac4 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.expect +++ b/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. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.html.expect index 879f3ec6f09..41f22a0291f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.html.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.html.expect @@ -53,7 +53,7 @@ AssumedConcurrentMethodFalseFalseFalseModifies clause has {:assume_concurrent} attribute.Manually review and test in a concurrent setting. AxiomWithStuffInItTrueTrueFalseDeclaration has explicit {:axiom} attribute.Provide a proof or test. AssertOnlyTrueFalseFalseAssertion has explicit temporary {:only} attribute.Remove the {:only} attribute. -MethodOnlyTrueFalseFalseMember has explicit temporary {:only} attribute.Remove the {:only} attribute. +MethodOnlyTrueFalseFalseMember has explicit temporary @VerifyOnly attribute.Remove the @VerifyOnly attribute. GenerateBytesWithAxiomTrueTrueTrueDeclaration has explicit {:axiom} attribute.Provide a proof or test. ExternFunctionWithAxiomTrueTrueTrueDeclaration has explicit {:axiom} attribute.Provide a proof or test. TTrueFalseFalseTrait method calls may not terminate (uses {:termination false}).Remove if possible. diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.md.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.md.expect index 3aaf017ad4d..6cc8e907844 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.md.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/auditor/TestAuditor.dfy.md.expect @@ -20,7 +20,7 @@ | AssumedConcurrentMethod | False | False | False | Modifies clause has `{:assume_concurrent}` attribute. | Manually review and test in a concurrent setting. | | AxiomWithStuffInIt | True | True | False | Declaration has explicit `{:axiom}` attribute. | Provide a proof or test. | | AssertOnly | True | False | False | Assertion has explicit temporary `{:only}` attribute. | Remove the `{:only}` attribute. | -| MethodOnly | True | False | False | Member has explicit temporary `{:only}` attribute. | Remove the `{:only}` attribute. | +| MethodOnly | True | False | False | Member has explicit temporary `@VerifyOnly` attribute. | Remove the `@VerifyOnly` attribute. | | GenerateBytesWithAxiom | True | True | True | Declaration has explicit `{:axiom}` attribute. | Provide a proof or test. | | ExternFunctionWithAxiom | True | True | True | Declaration has explicit `{:axiom}` attribute. | Provide a proof or test. | | T | True | False | False | Trait method calls may not terminate (uses `{:termination false}`). | Remove if possible. | diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4074.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4074.dfy.expect index 6473a6fb972..4950864d1ac 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4074.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4074.dfy.expect @@ -1,7 +1,7 @@ -git-issue-4074.dfy(23,11): Warning: Members with {:only} temporarily disable the verification of other members in the entire file -git-issue-4074.dfy(4,9): Warning: Members with {:only} temporarily disable the verification of other members in the entire file -git-issue-4074.dfy(4,14): Warning: {:only} on members does not support arguments -git-issue-4074.dfy(13,11): Warning: Members with {:only} temporarily disable the verification of other members in the entire file +git-issue-4074.dfy(23,11): Warning: Members with @VerifyOnly temporarily disable the verification of other members in the entire file +git-issue-4074.dfy(4,9): Warning: Members with @VerifyOnly temporarily disable the verification of other members in the entire file +git-issue-4074.dfy(4,14): Warning: @VerifyOnly on members does not support arguments +git-issue-4074.dfy(13,11): Warning: Members with @VerifyOnly temporarily disable the verification of other members in the entire file git-issue-4074.dfy(5,2): Error: assertion might not hold git-issue-4074.dfy(14,4): Error: assertion might not hold git-issue-4074.dfy(24,4): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5730/git-issue-5730.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5730/git-issue-5730.dfy index d70d2e2de0a..639cc50d34e 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5730/git-issue-5730.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5730/git-issue-5730.dfy @@ -2,7 +2,7 @@ // RUN: %diff "%s.expect" "%t" module X { - method {:only} VerifyMe() { + @VerifyOnly method VerifyMe() { assert false; // Should display an error } method DontVerifyMe() { diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5730/git-issue-5730.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5730/git-issue-5730.dfy.expect index 21f3a74d519..61b3253cb7a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5730/git-issue-5730.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5730/git-issue-5730.dfy.expect @@ -1,4 +1,4 @@ -git-issue-5730.dfy(5,11): Warning: Members with {:only} temporarily disable the verification of other members in the entire file +git-issue-5730.dfy(5,2): Warning: Members with @VerifyOnly temporarily disable the verification of other members in the entire file git-issue-5730-include.dfy(4,2): Error: assertion might not hold git-issue-5730.dfy(6,4): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/assumptions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/assumptions.dfy.expect index dfec83d8ebf..ace43beffcb 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/assumptions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/assumptions.dfy.expect @@ -9,7 +9,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. diff --git a/docs/dev/news/6146.fix b/docs/dev/news/6146.fix new file mode 100644 index 00000000000..ed4bd1a6025 --- /dev/null +++ b/docs/dev/news/6146.fix @@ -0,0 +1 @@ +Fix @VerifyOnly and migrated the new code to use it \ No newline at end of file