Fix incorrect missing {:axiom} warning message (#5307)

Fixes #5306

### Description
- Fix incorrect missing {:axiom} warning message that occurred when
having an opaque constant for a subset type.

### How has this been tested?
- Added a CLI test

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/AST/Members/MethodOrFunction.cs

@@ -38,7 +38,7 @@ public virtual void Resolve(ModuleResolver resolver) {
  }
 
  public void ResolveMethodOrFunction(INewOrOldResolver resolver) {
- if (Bodyless && !IsVirtual && !IsAbstract && !this.IsExtern(resolver.Options) && !this.IsExplicitAxiom()) {
+ if (!AutoGeneratedToken.Is(RangeToken) && Bodyless && !IsVirtual && !IsAbstract && !this.IsExtern(resolver.Options) && !this.IsExplicitAxiom()) {
  foreach (var ensures in Ens) {
  if (!ensures.IsExplicitAxiom() && !resolver.Options.Get(CommonOptionBag.AllowAxioms)) {
  resolver.Reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.none, ensures.Tok,

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/const.dfy

@@ -0,0 +1,4 @@
+// RUN: %testDafnyForEachResolver "%s" -- --allow-axioms=false
+
+type Even = x: int | x % 2 == 0
+opaque const ten: Even := 10

Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/const.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 2 verified, 0 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Verification.dfy.expect

@@ -20,7 +20,6 @@ Twostate-Verification.dfy(679,22): Warning: Argument to 'old' does not dereferen
 Twostate-Verification.dfy(680,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 Twostate-Verification.dfy(681,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 Twostate-Verification.dfy(682,22): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
-Twostate-Verification.dfy(189,23): Warning: This ensures clause is part of a bodyless function. Add the {:axiom} attribute to it or the enclosing function to suppress this warning
 Twostate-Verification.dfy(33,13): Warning: Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect
 Twostate-Verification.dfy(313,38): Error: assertion might not hold
 Twostate-Verification.dfy(337,23): Error: a precondition for this call could not be proved

docs/dev/news/5306.fix

@@ -0,0 +1 @@
+Stop giving an incorrect warning about a missing {:axiom} clause on an opaque constant.