Unknown Exception thrown for old in pure functions

[gottschali]

If one uses old in the postcondition of a pure function, a large unhandled exception is thrown. I think it would be preferable to have an error message indicating that old is not necessary in pure functions.

Example program:

package issue
type cell struct {
	value int
}
// @ pure
// @ decreases
// @ requires acc(c)
// @ ensures r == old(c.value)
func read(c *cell) (r int) {
	return c.value
}

Error:

Gobra 1.1-SNAPSHOT (@)
(c) Copyright ETH Zurich 2012 - 2024
15:22:49.119 [main] INFO viper.gobra.Gobra - Verifying package .. - issue [15:22:49]
15:22:52.174 [main] ERROR viper.gobra.GobraRunner$ - An unknown Exception was thrown.
15:22:52.175 [main] ERROR viper.gobra.GobraRunner$ - java.util.NoSuchElementException: key not found: old
java.util.concurrent.ExecutionException: java.util.NoSuchElementException: key not found: old
        at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:124)
        at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:193)
        at viper.silicon.Silicon.verify(Silicon.scala:205)
        at viper.silicon.Silicon.verify(Silicon.scala:163)
        at viper.gobra.backend.Silicon.$anonfun$verify$1(Silicon.scala:27)
        at scala.concurrent.Future$.$anonfun$apply$1(Future.scala:678)
        at scala.concurrent.impl.Promise$Transformation.run(Promise.scala:467)
        at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1095)
        at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:619)
        at java.base/java.lang.Thread.run(Thread.java:1447)
Caused by: java.util.NoSuchElementException: key not found: old
[more lines omitted]