Referencing old in pure method gives aborted exceptionally

[bobismijnnaam]

I try to verify the following code:

class MyClass {
  int x;
  requires Perm(x, 1);
  ensures x == \old(x);
  pure int foo() = x;
}

It's not very useful, and I don't know if \old is even supported in pure functions. So I don't necessarily need it to verify. But I do get the following exception:

Verification aborted exceptionally: java.util.concurrent.ExecutionException: java.util.NoSuchElementException: key not found: old
  Cause: java.util.NoSuchElementException: key not found: old
finished verify
Errors! (1)
WARNING: unspecified error exceptional.error
The final verdict is Fail
entire run took 4130 ms

Which I thought was a bit odd. I simple "old does not make sense in pure functions" would be better, if I understand correctly how old works.

[wytseoortwijn]

Indeed, \old is not supported in pure functions, as these are side-effect free. The error message should indeed be improved to make this clear.

[sjcjoosten]

Related to #194. Did #201 fix this? (Can someone test this again and close if it doesn't reproduce)

[Sophietje]

I tried but I still get the same error message.

[pieter-bos]

Seems to me we should just forbid using old in predicate specifications. I think for pure methods it's still unclear what to do anyway via #240, but we might as well just forbid it there also.