Unknown Exception thrown for old in pure functions #815
Description
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]