Fix null ref in covered tokens

Source/DafnyCore/AST/Members/Function.cs

@@ -96,7 +96,6 @@ public TailStatus
  public readonly Formal Result;
  public PreType ResultPreType;
  public readonly Type ResultType;
- public readonly Specification<FrameExpression> Reads;
  public Expression Body; // an extended expression; Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution
  public IToken /*?*/ ByMethodTok; // null iff ByMethodBody is null
  public BlockStmt /*?*/ ByMethodBody;

Source/DafnyCore/AST/Members/Method.cs

@@ -36,7 +36,6 @@ static Method() {
  public bool MustReverify;
  public bool IsEntryPoint = false;
  public readonly List<Formal> Outs;
- public readonly Specification<FrameExpression> Reads;
  public readonly Specification<FrameExpression> Mod;
  [FilledInDuringResolution] public bool IsRecursive;
  [FilledInDuringResolution] public bool IsTailRecursive;

Source/DafnyCore/AST/Members/MethodOrFunction.cs

@@ -93,9 +93,5 @@ public void ResolveMethodOrFunction(INewOrOldResolver resolver) {
  protected MethodOrFunction(RangeToken tok, Name name, bool hasStaticKeyword, bool isGhost, Attributes attributes, bool isRefining) : base(tok, name, hasStaticKeyword, isGhost, attributes, isRefining) {
  }
 
- public Specification<FrameExpression> Reads => this switch {
- Method m => m.Reads,
- Function f => f.Reads,
- _ => throw new cce.UnreachableException()
- };
+ public Specification<FrameExpression> Reads { get; set; }
 }

Source/DafnyCore/Generic/Node.cs

@@ -56,6 +56,9 @@ public abstract class Node : INode {
  public IEnumerable<IToken> CoveredTokens {
  get {
  var token = StartToken;
+ if (token == Token.NoToken) {
+ yield break;
+ }
  while (token.Prev != EndToken) {
  yield return token;
  token = token.Next;

Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs

@@ -40,6 +40,42 @@ public async Task MethodKeywordCodeAction() {
  Assert.Empty(completionList);
  }
 
+ [Fact]
+ public async Task TypeTestCodeAction() {
+ await SetUp(o => o.Set(CommonOptionBag.RelaxDefiniteAssignment, true));
+
+ MarkupTestFile.GetPositionsAndAnnotatedRanges(@"module M {
+ trait Object {
+ ghost function typeId() : (id: string)
+ }
+
+ type A extends Object {
+ ghost function typeId() : (id: string) { ""A"" }
+ }
+
+ type B extends Object {
+ ghost function typeId() : (id: string) { ""B"" }
+ }
+ type C extends Object {
+ ghost function typeId() : (id: string) { ""C"" }
+ }
+
+ lemma test(x: Object)
+ ensures multiset{x is A, x is B, x is C}[true] == 1
+ {
+ var _ := x.typeId();
+ if (x is A) {
+ assert x !is B.><
+ }
+ }
+}".TrimStart(), out var source, out var positions,
+ out var ranges);
+ var documentItem = await CreateOpenAndWaitForResolve(source);
+ var position = positions[0];
+ var completionList = await RequestCodeActionAsync(documentItem, new Range(position, position));
+ Assert.Empty(completionList);
+ }
+
  [Fact]
  public async Task GitIssue4401CorrectInsertionPlace() {
  await TestCodeAction(@"