Crash when translating UnboundedThreads.chalice

[viper-admin]

Created by @vakaras on 2015-06-26 10:19

The program translator component crashes when translating the chaliceSuite/examples/UnboundedThreads.chalice.

Minimal Chalice example:

#!Chalice
class C {

  method work(n: int)
  {
    var tks:seq<token<C.m>> := nil<token<C.m>>;
    assert acc(tks[*].joinable);
  }

  method m() {}

}

Stack trace:

[info]   [chalice2silver.error] java.util.NoSuchElementException: key not found: SpecialField(joinable,chalice.Type@3251976a,false)
[info] scala.collection.MapLike$class.default(MapLike.scala:228)
[info] scala.collection.AbstractMap.default(Map.scala:58)
[info] scala.collection.MapLike$class.apply(MapLike.scala:141)
[info] scala.collection.AbstractMap.apply(Map.scala:58)
[info] viper.chalice2sil.translation.ProgramTranslator.translateExp(ProgramTranslator.scala:568)
[info] viper.chalice2sil.translation.ProgramTranslator.translateStm(ProgramTranslator.scala:709)
[info] viper.chalice2sil.translation.ProgramTranslator$$anonfun$7.apply(ProgramTranslator.scala:695)
[info] viper.chalice2sil.translation.ProgramTranslator$$anonfun$7.apply(ProgramTranslator.scala:695)
[info] scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:244)
[info] scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:244)
[info] scala.collection.immutable.List.foreach(List.scala:318)
[info] scala.collection.TraversableLike$class.map(TraversableLike.scala:244)
[info] scala.collection.AbstractTraversable.map(Traversable.scala:105)
[info] viper.chalice2sil.translation.ProgramTranslator.translateBody(ProgramTranslator.scala:695)
[info] viper.chalice2sil.translation.ProgramTranslator$$anonfun$translate$3.apply(ProgramTranslator.scala:85)
[info] viper.chalice2sil.translation.ProgramTranslator$$anonfun$translate$3.apply(ProgramTranslator.scala:84)
[info] scala.collection.Iterator$class.foreach(Iterator.scala:727)
[info] scala.collection.AbstractIterator.foreach(Iterator.scala:1157)
[info] scala.collection.IterableLike$class.foreach(IterableLike.scala:72)
[info] scala.collection.AbstractIterable.foreach(Iterable.scala:54)
[info] viper.chalice2sil.translation.ProgramTranslator.translate(ProgramTranslator.scala:84)
[info] viper.chalice2sil.Chalice2SILFrontEnd.translate(Chalice2SILFrontend.scala:104)