Dafny does not provide a warning when using the old keyword on immutable values. This doesn't make sense and can lead to misunderstanding. Pointing this out in an analysis exposed via the IDE would clear this up.

For example, the following code verifies, and it's not immediately obvious why.

module Test {

  class C {
  }

  function arrSet(a: array<C>) : set<object>
    reads a
  {
    set i : int | 0 <= i < a.Length :: a[i]
  }

  method test(a: array<C>, i : int, x : C)
    modifies a
    requires 0 <= i < a.Length
    requires x !in arrSet(a)
  {
    a[i] := x;
    assert(arrSet(a) == arrSet(old(a)));
  }
}

The reason that assert(arrSet(a) == arrSet(old(a))); verifies is that old(a) refers to the reference, and not to the values in a. This is documented, but a linter pass warning about using old on an immutable value would be helpful.