Internal Error when mixing quantified permissions and predicates

[viper-admin]

Created by @vakaras on 2018-07-23 16:09

This program:

#!silver
field val: Int

domain Array {
    function loc(arr: Array, pos: Int): Ref
    function len(arr: Array): Int
}

predicate arrayacc(a: Array) {
    forall i: Int :: { loc(a, i) } 0 <= i && i < len(a) ==> acc(loc(a, i).val)
}

method solve1(fruits: Array)
    requires forall j: Int :: { loc(fruits, j) } 0 <= j && j < len(fruits) ==>
        (unfolding acc(arrayacc(fruits)) in true)
    ensures forall i: Int :: { loc(fruits, i) } 0 <= i && i < len(fruits) ==> true
{
}

gives the following stack trace:

java.lang.RuntimeException: Internal Error: variable i is already defined.
        at scala.sys.package$.error(package.scala:27)
        at viper.carbon.verifier.Environment.define(Environment.scala:65)
        at viper.carbon.modules.impls.DefaultExpModule$$anonfun$viper$carbon$modules$impls$DefaultExpModule$$checkDefinednessImpl$1.apply(DefaultExpModule.scala:343)
        at viper.carbon.modules.impls.DefaultExpModule$$anonfun$viper$carbon$modules$impls$DefaultExpModule$$checkDefinednessImpl$1.apply(DefaultExpModule.scala:343)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
        at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
        at scala.collection.AbstractTraversable.map(Traversable.scala:104)
        at viper.carbon.modules.impls.DefaultExpModule.viper$carbon$modules$impls$DefaultExpModule$$checkDefinednessImpl(DefaultExpModule.scala:343)
        at viper.carbon.modules.impls.DefaultExpModule.checkDefinedness(DefaultExpModule.scala:282)
        at viper.carbon.modules.impls.DefaultExpModule.checkDefinednessOfSpecAndInhale(DefaultExpModule.scala:440)
        at viper.carbon.modules.ExpModule$$anonfun$checkDefinednessOfExhaleSpecAndInhale$1.apply(ExpModule.scala:49)
        at viper.carbon.modules.ExpModule$$anonfun$checkDefinednessOfExhaleSpecAndInhale$1.apply(ExpModule.scala:48)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
        at scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
        at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
        at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
        at scala.collection.AbstractTraversable.map(Traversable.scala:104)
        at viper.carbon.modules.ExpModule$class.checkDefinednessOfExhaleSpecAndInhale(ExpModule.scala:48)
        at viper.carbon.modules.impls.DefaultExpModule.checkDefinednessOfExhaleSpecAndInhale(DefaultExpModule.scala:22)
        at viper.carbon.modules.impls.DefaultMainModule.translateMethodDeclCheckPosts(DefaultMainModule.scala:131)
        at viper.carbon.modules.impls.DefaultMainModule.translateMethodDecl(DefaultMainModule.scala:106)
        at viper.carbon.modules.impls.DefaultMainModule$$anonfun$5.apply(DefaultMainModule.scala:67)
        at viper.carbon.modules.impls.DefaultMainModule$$anonfun$5.apply(DefaultMainModule.scala:67)
        at scala.collection.TraversableLike$$anonfun$flatMap$1.apply(TraversableLike.scala:241)
        at scala.collection.TraversableLike$$anonfun$flatMap$1.apply(TraversableLike.scala:241)
        at scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
        at scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
        at scala.collection.TraversableLike$class.flatMap(TraversableLike.scala:241)
        at scala.collection.AbstractTraversable.flatMap(Traversable.scala:104)
        at viper.carbon.modules.impls.DefaultMainModule.translate(DefaultMainModule.scala:67)
        at viper.carbon.CarbonVerifier.verify(CarbonVerifier.scala:136)
        at viper.silver.frontend.DefaultFrontend$class.doVerify(Frontend.scala:236)
        at viper.carbon.CarbonFrontend.doVerify(Carbon.scala:26)
        at viper.silver.frontend.DefaultFrontend$class.verify(Frontend.scala:232)
        at viper.carbon.CarbonFrontend.verify(Carbon.scala:26)
        at viper.silver.frontend.SilFrontend$class.execute(SilFrontend.scala:152)
        at viper.carbon.CarbonFrontend.execute(Carbon.scala:26)
        at viper.carbon.Carbon$.main(Carbon.scala:20)
        at viper.carbon.Carbon.main(Carbon.scala)
        at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
        at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
        at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
        at java.lang.reflect.Method.invoke(Method.java:498)
        at com.martiansoftware.nailgun.NGSession.run(NGSession.java:280)