Do not crash when required parameters occur after optional ones (dafn…

…y-lang#5074) Fixes dafny-lang#4809 ### Description Do not crash when required parameters occur after optional ones ### How has this been tested? Added a littish 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>
Dargones · Feb 16, 2024 · be07874 · be07874
1 parent af84d77
commit be07874
Show file tree

Hide file tree

Showing 7 changed files with 18 additions and 9 deletions.
diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs
@@ -3341,16 +3341,14 @@ void ResolveActualParameters(ActualBindings bindings, List<Formal> formals, ITok
           substMap.Add(formal, n);
         } else {
           // parameter has no value
-          if (onlyPositionalArguments) {
-            // a simple error message has already been reported
-            Contract.Assert(simpleErrorReported);
-          } else {
+          if (!simpleErrorReported) {
             var formalDescription = whatKind + (context is Method ? " in-parameter" : " parameter");
             var nameWithIndex = formal.HasName && formal is not ImplicitFormal ? "'" + formal.Name + "'" : "";
             if (formals.Count > 1 || nameWithIndex == "") {
               nameWithIndex += nameWithIndex == "" ? "" : " ";
               nameWithIndex += $"at index {formalIndex}";
             }
+
             var message = $"{formalDescription} {nameWithIndex} requires an argument of type {formal.Type}";
             reporter.Error(MessageSource.Resolver, callTok, message);
           }

diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs
@@ -139,16 +139,14 @@ void ResolveActualParameters(ActualBindings bindings, List<Formal> formals, ITok
           substMap.Add(formal, n);
         } else {
           // parameter has no value
-          if (onlyPositionalArguments) {
-            // a simple error message has already been reported
-            Contract.Assert(simpleErrorReported);
-          } else {
+          if (!simpleErrorReported) {
             var formalDescription = whatKind + (context is Method ? " in-parameter" : " parameter");
             var nameWithIndex = formal.HasName && formal is not ImplicitFormal ? "'" + formal.Name + "'" : "";
             if (formals.Count > 1 || nameWithIndex == "") {
               nameWithIndex += nameWithIndex == "" ? "" : " ";
               nameWithIndex += $"at index {formalIndex}";
             }
+
             var message = $"{formalDescription} {nameWithIndex} requires an argument of type {formal.Type}";
             ReportError(callTok, message);
           }

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy
@@ -0,0 +1,7 @@
+// RUN: %testDafnyForEachResolver "%s" --expect-exit-code=2
+
+function SumFromTo(sequence: nat -> real, start: nat := 0, end: nat): real
+
+function PartialSums(sequence: nat -> real): nat -> real {
+  (n: nat) => SumFromTo(sequence, n)
+}
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy.expect
@@ -0,0 +1,2 @@
+defaultParameterResolution.dfy(6,23): Error: function parameter 'end' at index 2 requires an argument of type nat
+1 resolution/type errors detected in defaultParameterResolution.dfy
diff --git a/...grationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy.refresh.expect b/...grationTests/TestFiles/LitTests/LitTest/ast/defaultParameterResolution.dfy.refresh.expect
@@ -0,0 +1,3 @@
+defaultParameterResolution.dfy(3,59): Error: a required parameter must precede all optional parameters
+defaultParameterResolution.dfy(6,23): Error: function parameter 'end' at index 2 requires an argument of type nat
+2 resolution/type errors detected in defaultParameterResolution.dfy
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/DefaultParameters.dfy
@@ -600,4 +600,4 @@ module ExtremeNat {
   lemma TestLeastZero(y: int, z: int, v: int, w: int, a: int, b: int, o: nat) {
     assert Q#[o](b); // error: does not hold for o == 0
   }
-}
+}
diff --git a/docs/dev/news/4809.fix b/docs/dev/news/4809.fix
@@ -0,0 +1 @@
+Dafny no longer crashes when required parameters occur after optional ones.
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		defaultParameterResolution.dfy(6,23): Error: function parameter 'end' at index 2 requires an argument of type nat
		1 resolution/type errors detected in defaultParameterResolution.dfy
-Original file line number
+Diff line change
@@ Expand Up / @@ -600,4 +600,4 @@ module ExtremeNat { @@
       lemma TestLeastZero(y: int, z: int, v: int, w: int, a: int, b: int, o: nat) {
         assert Q#[o](b); // error: does not hold for o == 0
       }
-    }
+    }
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		Dafny no longer crashes when required parameters occur after optional ones.