Yields variables are nameable in preconditions

[bobismijnnaam]

In VerCors 2.0.0 alpha 6, yields variables are nameable in preconditions. The following verifies:

class Test {
  yields int[] indegree;
  requires indegree != null ** indegree.length > 0;
  requires Perm(indegree[0], write) ** indegree[0] == 0;
  boolean m() {
    assert \old(indegree[0]) == 0;
  }
}

Instead, I would expect one, possibly two, errors:

• indegree does not have a value in the method pre-state, so that should be an error
• therefore it also cannot be mentioned in \old expressions, so that could also be an error.

In this specific case it'd be fine if the precondition error makes the error about the usage of a yields var in \old disappear. However in other cases that should also be an error.