Skip to content

Commit

Permalink
Fix: Potential empty collection exception
Browse files Browse the repository at this point in the history
This PR used to fix #2833, but I am no longer able to reproduce the problem in the latest master anyway, so I cannot add a test that this PR would solve at this point.
Still, I think it's safer to have a safeguard. Otherwise, when `result` is `null` and `typeArgs` is empty, it will continue to throw an exception
  • Loading branch information
MikaelMayer committed Oct 4, 2022
1 parent 9413c19 commit 5333b41
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 1 deletion.
6 changes: 5 additions & 1 deletion Source/DafnyCore/AST/Types.cs
Original file line number Diff line number Diff line change
Expand Up @@ -2018,7 +2018,11 @@ public static string PrettyArrowTypeName(string arrow, List<Type> typeArgs, Type
s += Util.Comma(typeArgs.Take(arity), arg => arg.TypeName(context, parseAble));
if (domainNeedsParens) { s += ")"; }
s += " " + arrow + " ";
s += (result ?? typeArgs.Last()).TypeName(context, parseAble);
if (result != null || typeArgs.Count >= 1) {
s += (result ?? typeArgs.Last()).TypeName(context, parseAble);
} else {
s += "<unable to infer result type>";
}
return s;
}

Expand Down
19 changes: 19 additions & 0 deletions Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,25 @@ decreases y
await AssertNoDiagnosticsAreComing(CancellationToken);
}


[TestMethod]
public async Task OpeningFunctionWithErrorDoesNotCrash() {
var source = @"
datatype ParseResult<T> = Success(value: T) | Failure
predicate FixMapInner() {
forall callback: (string, nat) --> ParseResult<T>, fun: string, u: nat |
&& fun in underlying.Keys
&& FixMapSpecInner(underlying.Keys, |input|, callback, u)
:: underlying[fun].requires(callback, u)
}".TrimStart();
var documentItem = CreateTestDocument(source);
await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken);
Assert.AreEqual(1, diagnostics.Length);
await AssertNoDiagnosticsAreComing(CancellationToken);
}

[TestMethod]
public async Task OpeningOpaqueFunctionWorks() {
var source = @"
Expand Down

0 comments on commit 5333b41

Please sign in to comment.