Fix call stmt reporting

Source/DafnyCore/AST/Statements/Assignment/AssignStatement.cs

@@ -177,7 +177,7 @@ public override void Resolve(ModuleResolver resolver, ResolutionContext resoluti
         foreach (var ll in Lhss) {
           resolvedLhss.Add(ll.Resolved);
         }
-        CallStmt a = new CallStmt(Origin, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok.Center);
+        CallStmt a = new CallStmt(Origin, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok.ReportingRange);
         a.OriginalInitialLhs = OriginalInitialLhs;
         ResolvedStatements.Add(a);
       }

Source/DafnyCore/AST/Statements/Methods/CallStmt.cs

@@ -30,11 +30,9 @@ public override IEnumerable<IdentifierExpr> GetAssignedLocals() {
   public Expression Receiver => MethodSelect.Obj;
   public MethodOrConstructor Method => (MethodOrConstructor)MethodSelect.Member;
 
-  public CallStmt(IOrigin rangeOrigin, List<Expression> lhs, MemberSelectExpr memSel, List<ActualBinding> args, Token overrideToken = null)
-    : base(
-      /* it would be better if the correct rangeOrigin was passed in,
-       then the parameter overrideToken would become obsolete */
-      new OverrideCenter(rangeOrigin, overrideToken ?? memSel.EndToken.Next)) {
+  public CallStmt(IOrigin rangeOrigin, List<Expression> lhs, MemberSelectExpr memSel, List<ActualBinding> args,
+      TokenRange overrideToken = null)
+    : base(overrideToken == null ? rangeOrigin : new OverrideCenter(rangeOrigin, overrideToken)) {
     Contract.Requires(rangeOrigin != null);
     Contract.Requires(cce.NonNullElements(lhs));
     Contract.Requires(memSel != null);
@@ -61,8 +59,8 @@ public CallStmt(Cloner cloner, CallStmt original) : base(cloner, original) {
   /// This constructor is intended to be used when constructing a resolved CallStmt. The "args" are expected
   /// to be already resolved, and are all given positionally.
   /// </summary>
-  public CallStmt(IOrigin rangeOrigin, List<Expression> lhs, MemberSelectExpr memSel, List<Expression> args)
-    : this(rangeOrigin, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e))) {
+  public CallStmt(IOrigin rangeOrigin, List<Expression> lhs, MemberSelectExpr memSel, List<Expression> args, TokenRange overrideToken = null)
+    : this(rangeOrigin, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e)), overrideToken) {
     Bindings.AcceptArgumentExpressionsAsExactParameterList();
   }
 

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

@@ -123,7 +123,7 @@ public override void GenResolve(INewOrOldResolver resolver, ResolutionContext re
               if (revealCallee != null) {
                 var call = new CallStmt(Origin, [],
                   revealCallee,
-                  [], effectiveExpr.Center);
+                  (List<Expression>)[], effectiveExpr.ReportingRange);
                 ResolvedStatements.Add(call);
               }
             } else {

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -4423,7 +4423,7 @@ public void ResolveTypeRhs(TypeRhs rr2, Statement stmt, ResolutionContext resolu
                 Contract.Assert(callLhs.ResolvedExpression is MemberSelectExpr);  // since ResolveApplySuffix succeeded and call.Lhs denotes an expression (not a module or a type)
                 var methodSel = (MemberSelectExpr)callLhs.ResolvedExpression;
                 if (methodSel.Member is MethodOrConstructor) {
-                  allocateClass.InitCall = new CallStmt(stmt.Origin, [], methodSel, allocateClass.Bindings.ArgumentBindings, initCallTok.Center);
+                  allocateClass.InitCall = new CallStmt(stmt.Origin, [], methodSel, allocateClass.Bindings.ArgumentBindings, initCallTok.ReportingRange);
                   ResolveCallStmt(allocateClass.InitCall, resolutionContext, allocateClass.Type);
                 } else {
                   reporter.Error(MessageSource.Resolver, initCallTok, "object initialization must denote an initializing method or constructor ({0})", initCallName);

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs

@@ -703,7 +703,7 @@ private void ResolveUpdateStmt(AssignStatement update, ResolutionContext resolut
         } else if (ErrorCount == errorCountBeforeCheckingStmt) {
           // a call statement
           var resolvedLhss = update.Lhss.ConvertAll(ll => ll.Resolved);
-          var a = new CallStmt(update.Origin, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok.Center);
+          var a = new CallStmt(update.Origin, resolvedLhss, methodCallInfo.Callee, methodCallInfo.ActualParameters, methodCallInfo.Tok.ReportingRange);
           a.OriginalInitialLhs = update.OriginalInitialLhs;
           update.ResolvedStatements.Add(a);
         }
@@ -1204,7 +1204,7 @@ public void ResolveTypeRhs(TypeRhs rr, Statement stmt, ResolutionContext resolut
               Contract.Assert(callLhs.ResolvedExpression is MemberSelectExpr);  // since ResolveApplySuffix succeeded and call.Lhs denotes an expression (not a module or a type)
               var methodSel = (MemberSelectExpr)callLhs.ResolvedExpression;
               if (methodSel.Member is MethodOrConstructor) {
-                allocateClass.InitCall = new CallStmt(stmt.Origin, [], methodSel, allocateClass.Bindings.ArgumentBindings, initCallTok.Center);
+                allocateClass.InitCall = new CallStmt(stmt.Origin, [], methodSel, allocateClass.Bindings.ArgumentBindings, initCallTok.ReportingRange);
                 ResolveCallStmt(allocateClass.InitCall, resolutionContext, allocateClass.Type);
               } else {
                 ReportError(initCallTok, "object initialization must denote an initializing method or constructor ({0})", initCallName);

Source/DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs

@@ -332,8 +332,8 @@ public static HideRevealStmt BuildRevealStmt(Function func, IOrigin tok, ModuleD
     rr.TypeApplicationJustMember = [];
     rr.TypeApplicationAtEnclosingClass = args;
 
-    var call = new CallStmt(func.Origin, [], rr, [],
-      func.Center);
+    var call = new CallStmt(func.Origin, [], rr, (List<Expression>)[],
+      func.ReportingRange);
     call.IsGhost = true;
     call.Bindings.AcceptArgumentExpressionsAsExactParameterList([]);
 

Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs

@@ -179,7 +179,7 @@ internal override void PostResolve(Program program) {
               }
           }
 
-          var callStmt = new CallStmt(tok, lhss, methodSelectExpr, []);
+          var callStmt = new CallStmt(tok, lhss, methodSelectExpr, (List<Expression>)[]);
           tryBodyStatements.Add(callStmt);
 
           Statement passedStmt = Statement.CreatePrintStmt(tok, Expression.CreateStringLiteral(tok, "PASSED\n"));

Source/DafnyTestGeneration.Test/Various.cs

@@ -619,7 +619,7 @@ module Math {
     public async Task FunctionMethodShortCircuit(List<Action<DafnyOptions>> optionSettings) {
       var source = @"
 module ShortCircuit {
-  function {:testEntry} Or(a:bool):bool {
+  function {:testEntry} Or(a:bool): bool {
     a || OnlyFalse(a)
   }
   function {:testInline} OnlyFalse(a:bool):bool

Source/DafnyTestGeneration/Inlining/FunctionCallToMethodCallRewriter.cs

@@ -70,7 +70,8 @@ public override Statement CloneStmt(Statement stmt, bool isReference) {
         memberSelectExpr.TypeApplicationJustMember = funcCallExpr.TypeApplication_JustFunction;
         newResolvedStmts.Add(new CallStmt(stmt.Origin,
           updateStmt.Lhss.Select(lhs => CloneExpr(lhs.Resolved)).ToList(), memberSelectExpr,
-          funcCallExpr.Args.ConvertAll(e => CloneExpr(e.Resolved))));
+          funcCallExpr.Args.ConvertAll(e => CloneExpr(e.Resolved)),
+          memberSelectExpr.EndToken.Next.ReportingRange));
       } else {
         newResolvedStmts.Add(resolvedStmt);
       }

Source/DafnyTestGeneration/Inlining/RemoveShortCircuitRewriter.cs

@@ -225,7 +225,7 @@ private Statement CloneReturnStmt(ReturnStmt returnStatement) {
   }
 
   private Statement CloneCallStmt(CallStmt callStmt) {
-    return new CallStmt(callStmt.Origin, CloneExpressionList(callStmt.Lhs), callStmt.MethodSelect, CloneExpressionList(callStmt.Args));
+    return new CallStmt(callStmt.Origin, CloneExpressionList(callStmt.Lhs), callStmt.MethodSelect, CloneExpressionList(callStmt.Args), callStmt.MethodSelect.EndToken.Next.ReportingRange);
   }
 
   private Statement CloneNestedMatchStmt(NestedMatchStmt nestedMatchStatement) {