@pure function with inner functions causes a crash

[mario-bucev]

The following causes a MatchError on IsPure

import stainless._
import stainless.lang._
import stainless.annotation._

object PureFnWithInnerFn {
  @pure
  def outer: Unit = {
    def inner: Unit = ()
  }
}

(seems to be a minor oversight in ImperativeCodeElimination which should filter out the IsPure flags on transformed inner functions)

Stacktrace

scala.MatchError: IsPure (of class stainless.extraction.imperative.Trees$IsPure$)
	at inox.ast.TreeDeconstructor.deconstruct(Deconstructors.scala:526)
	at inox.ast.TreeDeconstructor.deconstruct$(Deconstructors.scala:21)
	at stainless.extraction.oo.ConcreteTreeDeconstructor.stainless$ast$TreeDeconstructor$$super$deconstruct(Trees.scala:486)
	at stainless.ast.TreeDeconstructor.deconstruct(Deconstructors.scala:231)
	at stainless.ast.TreeDeconstructor.deconstruct$(Deconstructors.scala:6)
	at stainless.extraction.oo.ConcreteTreeDeconstructor.stainless$extraction$termination$TreeDeconstructor$$super$deconstruct(Trees.scala:486)
	at stainless.extraction.termination.TreeDeconstructor.deconstruct(Trees.scala:37)
	at stainless.extraction.termination.TreeDeconstructor.deconstruct$(Trees.scala:31)
	at stainless.extraction.oo.ConcreteTreeDeconstructor.stainless$extraction$trace$TreeDeconstructor$$super$deconstruct(Trees.scala:486)
	at stainless.extraction.trace.TreeDeconstructor.deconstruct(Trees.scala:35)
	at stainless.extraction.trace.TreeDeconstructor.deconstruct$(Trees.scala:29)
	at stainless.extraction.oo.ConcreteTreeDeconstructor.stainless$extraction$inlining$TreeDeconstructor$$super$deconstruct(Trees.scala:486)
	at stainless.extraction.inlining.TreeDeconstructor.deconstruct(Trees.scala:38)
	at stainless.extraction.inlining.TreeDeconstructor.deconstruct$(Trees.scala:31)
	at stainless.extraction.oo.ConcreteTreeDeconstructor.stainless$extraction$oo$TreeDeconstructor$$super$deconstruct(Trees.scala:486)
	at stainless.extraction.oo.TreeDeconstructor.deconstruct(Trees.scala:482)
	at stainless.extraction.oo.TreeDeconstructor.deconstruct$(Trees.scala:426)
	at stainless.extraction.oo.ConcreteTreeDeconstructor.deconstruct(Trees.scala:486)
	at inox.transformers.Transformer.transform(Transformer.scala:141)
	at inox.transformers.Transformer.transform$(Transformer.scala:6)
	at stainless.extraction.oo.ConcreteTreeTransformer.inox$transformers$TreeTransformer$$super$transform(Trees.scala:518)
	at inox.transformers.TreeTransformer.transform(Transformer.scala:226)
	at inox.transformers.TreeTransformer.transform$(Transformer.scala:204)
	at stainless.extraction.oo.ConcreteTreeTransformer.transform(Trees.scala:518)
	at inox.transformers.TreeTransformer.transform(Transformer.scala:227)
	at inox.transformers.TreeTransformer.transform$(Transformer.scala:204)
	at stainless.extraction.oo.ConcreteTreeTransformer.transform(Trees.scala:518)
	at stainless.extraction.oo.ConcreteTreeTransformer.transform(Trees.scala:518)
	at inox.transformers.Transformer.$anonfun$6(Transformer.scala:82)
	at scala.collection.immutable.List.map(List.scala:246)
	at scala.collection.immutable.List.map(List.scala:79)
	at inox.transformers.Transformer.transform(Transformer.scala:85)
	at inox.transformers.Transformer.transform$(Transformer.scala:6)
	at stainless.extraction.oo.ConcreteTreeTransformer.stainless$transformers$Transformer$$super$transform(Trees.scala:518)
	at stainless.extraction.oo.ConcreteTreeTransformer.stainless$transformers$Transformer$$super$transform(Trees.scala:518)
	at stainless.transformers.Transformer.transform(Transformer.scala:63)
	at stainless.transformers.Transformer.transform$(Transformer.scala:8)
	at stainless.extraction.oo.ConcreteTreeTransformer.inox$transformers$TreeTransformer$$super$transform(Trees.scala:518)
	at inox.transformers.TreeTransformer.transform(Transformer.scala:220)
	at inox.transformers.TreeTransformer.transform$(Transformer.scala:204)
	at stainless.extraction.imperative.ImperativeCleanup$TransformerContext.transform(ImperativeCleanup.scala:98)
	at inox.transformers.TreeTransformer.transform(Transformer.scala:221)
	at inox.transformers.TreeTransformer.transform$(Transformer.scala:204)
	at stainless.extraction.oo.ConcreteTreeTransformer.transform(Trees.scala:518)
	at stainless.extraction.oo.ConcreteTreeTransformer.transform(Trees.scala:518)
	at inox.transformers.DefinitionTransformer.transform(Transformer.scala:181)
	at inox.transformers.DefinitionTransformer.transform$(Transformer.scala:170)
	at stainless.extraction.oo.ConcreteTreeTransformer.transform(Trees.scala:518)
	at stainless.extraction.SimplePhase.extractFunction(ExtractionPipeline.scala:153)
	at stainless.extraction.SimplePhase.extractFunction$(ExtractionPipeline.scala:147)
	at stainless.extraction.imperative.ImperativeCleanup.extractFunction(ImperativeCleanup.scala:140)
	at stainless.extraction.imperative.ImperativeCleanup.extractFunction(ImperativeCleanup.scala:126)
	at stainless.extraction.CachingPhase.$anonfun$3$$anonfun$1(ExtractionPipeline.scala:102)
	at stainless.extraction.utils.ConcurrentCache.cached(ConcurrentCaches.scala:26)
	at stainless.extraction.ExtractionCaches$ExtractionCache.cached(ExtractionCaches.scala:165)
	at stainless.extraction.CachingPhase.$anonfun$1(ExtractionPipeline.scala:102)
	at scala.collection.Iterator$$anon$9.next(Iterator.scala:575)
	at scala.collection.immutable.List.prependedAll(List.scala:153)
	at scala.collection.immutable.List$.from(List.scala:684)
	at scala.collection.immutable.List$.from(List.scala:681)
	at scala.collection.IterableFactory$Delegate.from(Factory.scala:288)
	at scala.collection.immutable.Iterable$.from(Iterable.scala:35)
	at scala.collection.immutable.Iterable$.from(Iterable.scala:32)
	at scala.collection.IterableFactory$Delegate.from(Factory.scala:288)
	at scala.collection.IterableOps.map(Iterable.scala:671)
	at scala.collection.IterableOps.map$(Iterable.scala:671)
	at scala.collection.AbstractIterable.map(Iterable.scala:919)
	at stainless.extraction.CachingPhase.extractSymbols(ExtractionPipeline.scala:102)
	at stainless.extraction.CachingPhase.extractSymbols$(ExtractionPipeline.scala:82)
	at stainless.extraction.imperative.ImperativeCleanup.stainless$extraction$oo$CachingPhase$$super$extractSymbols(ImperativeCleanup.scala:17)
	at stainless.extraction.imperative.ImperativeCleanup.stainless$extraction$oo$CachingPhase$$super$extractSymbols(ImperativeCleanup.scala:17)
	at stainless.extraction.oo.CachingPhase.extractSymbols(ExtractionPipeline.scala:28)
	at stainless.extraction.oo.CachingPhase.extractSymbols$(ExtractionPipeline.scala:13)
	at stainless.extraction.imperative.ImperativeCleanup.extractSymbols(ImperativeCleanup.scala:17)
	at stainless.extraction.imperative.ImperativeCleanup.extractSymbols(ImperativeCleanup.scala:17)
	at stainless.extraction.CachingPhase.extract(ExtractionPipeline.scala:97)
	at stainless.extraction.CachingPhase.extract$(ExtractionPipeline.scala:82)
	at stainless.extraction.imperative.ImperativeCleanup.extract(ImperativeCleanup.scala:17)
	at stainless.extraction.utils.DebugPipeline.extract$$anonfun$2$$anonfun$1(DebugPipeline.scala:136)
	at scala.util.Try$.apply(Try.scala:210)
	at inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
	at inox.utils.TimerStorage.run(Timer.scala:88)
	at stainless.extraction.utils.DebugPipeline.extract$$anonfun$1(DebugPipeline.scala:136)
	at stainless.extraction.utils.DebugSymbols.debug(DebugPipeline.scala:64)
	at stainless.extraction.utils.DebugSymbols.debug$(DebugPipeline.scala:29)
	at stainless.extraction.utils.DebugPipeline.debug(DebugPipeline.scala:124)
	at stainless.extraction.utils.DebugPipeline.extract(DebugPipeline.scala:137)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
	at stainless.extraction.ExtractionPipeline$AndThenImpl$1.extract(ExtractionPipeline.scala:30)
	at stainless.ComponentRun.extract(Component.scala:87)
	at stainless.ComponentRun.extract$(Component.scala:47)
	at stainless.verification.VerificationRun.extract(VerificationComponent.scala:53)
	at stainless.ComponentRun.apply(Component.scala:97)
	at stainless.ComponentRun.apply$(Component.scala:47)
	at stainless.verification.VerificationRun.apply(VerificationComponent.scala:53)
	at stainless.frontend.BatchedCallBack.$anonfun$3(BatchedCallBack.scala:109)
	at scala.collection.immutable.List.map(List.scala:246)
	at scala.collection.immutable.List.map(List.scala:79)
	at stainless.frontend.BatchedCallBack.endExtractions(BatchedCallBack.scala:110)
	at stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:34)
	at java.lang.Thread.run(Thread.java:748)