Renamed INode.RangeToken property to .Origin

.github/workflows/doc-tests.yml

@@ -25,7 +25,15 @@ jobs:
     if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
     runs-on: ubuntu-latest
 
-    steps:
+    steps: 
+    # The Windows image was recently updated with a .NET 9 CLI which made CI fail, 
+    # We added a global.json to force it to use any .NET CLI with 8 as a major version
+    - name: Setup dotnet
+      uses: actions/setup-dotnet@v4
+      with:
+        dotnet-version: 8.0.x
+    # If we do not also install .NET 6 as well, then our doc-tests fail for an unknown reason
+    # Failing run: https://github.com/dafny-lang/dafny/actions/runs/12276984671/job/34255376460
     - name: Setup dotnet
       uses: actions/setup-dotnet@v4
       with:

.github/workflows/runtime-tests.yml

@@ -5,7 +5,7 @@ on:
   pull_request:
     branches: [ master, main-* ]
   merge_group:
-
+  
 concurrency:
   group: ${{ github.workflow }}-${{ github.ref }}
   cancel-in-progress: true
@@ -25,6 +25,18 @@ jobs:
         uses: actions/checkout@v4
         with:
           submodules: true
+      # The Windows image was recently updated with a .NET 9 CLI which made CI fail, 
+      # We added a global.json to force it to use any .NET CLI with 8 as a major version
+      - name: Setup dotnet
+        uses: actions/setup-dotnet@v4
+        with:
+          dotnet-version: 8.0.x
+      # If we do not also install .NET 6 as well, then our doc-tests fail for an unknown reason
+      # Failing run: https://github.com/dafny-lang/dafny/actions/runs/12276984671/job/34255376460
+      - name: Setup dotnet
+        uses: actions/setup-dotnet@v4
+        with:
+          dotnet-version: 6.0.x
       - name: Set up JDK 18
         uses: actions/setup-java@v4
         with:

Source/DafnyCore.Test/ClonerTest.cs

@@ -27,11 +27,11 @@ public void ClonerKeepsBodyStartTok() {
     var rangeToken = new RangeToken(Token.NoToken, Token.NoToken);
     var specificationFrame = new LiteralExpr(Microsoft.Dafny.Token.NoToken, 1);
     var formal1 = new Formal(Token.NoToken, "a", Microsoft.Dafny.Type.Bool, true, false, null) {
-      RangeToken = new RangeToken(tokenBodyStart, tokenBodyStart),
+      Origin = new RangeToken(tokenBodyStart, tokenBodyStart),
       IsTypeExplicit = true
     };
     var formal2 = new Formal(Token.NoToken, "b", Microsoft.Dafny.Type.Bool, true, false, null) {
-      RangeToken = new RangeToken(tokenBodyStart, tokenBodyStart),
+      Origin = new RangeToken(tokenBodyStart, tokenBodyStart),
       IsTypeExplicit = false
     };
     var dummyDecl = new Method(rangeToken, new Name(rangeToken, "hello"),
@@ -45,9 +45,9 @@ public void ClonerKeepsBodyStartTok() {
     var cloner = new Cloner();
     var dummyDecl2 = cloner.CloneMethod(dummyDecl);
     Assert.Equal(2, dummyDecl2.BodyStartTok.line);
-    Assert.Equal(2, dummyDecl2.Ins[0].RangeToken.StartToken.line);
+    Assert.Equal(2, dummyDecl2.Ins[0].Origin.StartToken.line);
     Assert.True(dummyDecl2.Ins[0].IsTypeExplicit);
-    Assert.Equal(2, dummyDecl2.Ins[1].RangeToken.StartToken.line);
+    Assert.Equal(2, dummyDecl2.Ins[1].Origin.StartToken.line);
     Assert.False(dummyDecl2.Ins[1].IsTypeExplicit);
   }
 }

Source/DafnyCore.Test/NodeTests.cs

@@ -7,12 +7,12 @@ public class NodeTests {
 
   class ConcreteNode : Node {
     public ConcreteNode(RangeToken rangeOrigin, IEnumerable<INode>? children = null) {
-      RangeToken = rangeOrigin;
+      Origin = rangeOrigin;
       Children = children ?? Enumerable.Empty<INode>();
     }
 
-    public override RangeToken RangeToken { get; set; }
-    public override IOrigin Tok => RangeToken.StartToken;
+    public override RangeToken Origin { get; set; }
+    public override IOrigin Tok => Origin.StartToken;
     public override IEnumerable<INode> Children { get; }
     public override IEnumerable<INode> PreResolveChildren => Children;
   }

Source/DafnyCore/AST/Attributes.cs

@@ -306,7 +306,7 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib
     var bindings = atAttribute.UserSuppliedPreResolveBindings;
 
     if (name == null) {
-      program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, "Attribute not recognized: " + atAttribute.ToString());
+      program.Reporter.Error(MessageSource.Resolver, atAttribute.Origin, "Attribute not recognized: " + atAttribute.ToString());
       return null;
     }
 
@@ -316,7 +316,7 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib
     }
 
     if (!builtinSyntax.CanBeApplied(attributeHost)) {
-      program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, UserSuppliedAtAttribute.AtName + atAttribute.UserSuppliedName + " attribute cannot be applied to " + attributeHost.WhatKind);
+      program.Reporter.Error(MessageSource.Resolver, atAttribute.Origin, UserSuppliedAtAttribute.AtName + atAttribute.UserSuppliedName + " attribute cannot be applied to " + attributeHost.WhatKind);
     }
 
     var resolver = new ModuleResolver(new ProgramResolver(program), program.Options) {
@@ -614,7 +614,7 @@ private static void ResolveLikeDatatypeConstructor(Program program, Formal[] for
     // Verify that provided arguments are given literally
     foreach (var binding in bindings.ArgumentBindings) {
       if (binding.Actual is not LiteralExpr) {
-        program.Reporter.Error(MessageSource.Resolver, binding.Actual.RangeToken, $"Argument to attribute {attrName} must be a literal");
+        program.Reporter.Error(MessageSource.Resolver, binding.Actual.Origin, $"Argument to attribute {attrName} must be a literal");
       }
     }
   }