Wrong computation of capturedVariables

[jcp19]

In the following snippet, Gobra considers x to be a captured variable:

var x /*@@@*/ int = 1

func test() {
	f := func /*@ g @*/ () int {
		return x
	}
}

Because of this, Gobra crashes with the following stack trace:

[info] An unknown Exception was thrown.
[info] java.util.concurrent.ExecutionException: java.util.NoSuchElementException
[info] java.util.concurrent.ExecutionException: java.util.concurrent.ExecutionException: java.util.NoSuchElementException
[info] 	at java.base/java.util.concurrent.FutureTask.report(FutureTask.java:122)
[info] 	at java.base/java.util.concurrent.FutureTask.get(FutureTask.java:191)
[info] 	at viper.silicon.Silicon.verify(Silicon.scala:198)
[info] 	at viper.silicon.Silicon.verify(Silicon.scala:156)
[info] 	at viper.gobra.backend.Silicon.$anonfun$verify$1(Silicon.scala:27)
[info] 	at scala.concurrent.Future$.$anonfun$apply$1(Future.scala:672)
[info] 	at scala.concurrent.impl.Promise$Transformation.run(Promise.scala:431)
[info] 	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
[info] 	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
[info] 	at java.base/java.lang.Thread.run(Thread.java:834)
[info] Caused by: java.util.concurrent.ExecutionException: java.util.NoSuchElementException
[info] 	at java.base/java.util.concurrent.ForkJoinTask.get(ForkJoinTask.java:1006)
[info] 	at viper.silicon.verifier.DefaultMainVerifier.$anonfun$verify$9(DefaultMainVerifier.scala:268)
[info] 	at scala.collection.immutable.List.flatMap(List.scala:293)
[info] 	at scala.collection.immutable.List.flatMap(List.scala:79)
[info] 	at viper.silicon.verifier.DefaultMainVerifier.verify(DefaultMainVerifier.scala:268)
[info] 	at viper.silicon.Silicon.viper$silicon$Silicon$$runVerifier(Silicon.scala:239)
[info] 	at viper.silicon.Silicon$$anon$1.call(Silicon.scala:192)
[info] 	at viper.silicon.Silicon$$anon$1.call(Silicon.scala:191)
[info] 	at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
[info] 	... 3 common frames omitted
[info] Caused by: java.util.NoSuchElementException: null
[info] 	at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance0(Native Method)
[info] 	at java.base/jdk.internal.reflect.NativeConstructorAccessorImpl.newInstance(NativeConstructorAccessorImpl.java:62)
[info] 	at java.base/jdk.internal.reflect.DelegatingConstructorAccessorImpl.newInstance(DelegatingConstructorAccessorImpl.java:45)
[info] 	at java.base/java.lang.reflect.Constructor.newInstance(Constructor.java:490)
[info] 	at java.base/java.util.concurrent.ForkJoinTask.getThrowableException(ForkJoinTask.java:603)
[info] 	... 12 common frames omitted
[info] Caused by: java.util.NoSuchElementException: key not found: x_41fccf1_G
[info] 	at scala.collection.immutable.ListMap$Node.applyInternal(ListMap.scala:155)
[info] 	at scala.collection.immutable.ListMap$Node.apply(ListMap.scala:152)
[info] 	at viper.silicon.state.MapBackedStore.apply(Store.scala:40)
[info] 	at viper.silicon.rules.evaluator$.eval2(Evaluator.scala:161)
[info] 	at viper.silicon.rules.evaluator$.eval3(Evaluator.scala:129)
[info] 	at viper.silicon.rules.evaluator$.eval(Evaluator.scala:90)

I will provide a fix to this issue shortly

[Felalolf]

Ah, took me a while to understand what is going on. X is captured by the closure, but the closure should only be parameterized by local captured variables, which wasn't.