type checker assertion failure is possible

[viper-admin]

Created by @alexanderjsummers on 2017-05-15 17:02
Last updated on 2018-10-15 15:36

When running the following:

#!scala



domain Array {
  function loc(a: Array, i: Int): Ref
  function len(a: Array): Int
  function first(r: Ref): Array
  function second(r: Ref): Int

  axiom all_diff {
    forall a: Array, i: Int :: {loc(a, i)}
      first(loc(a, i)) == a && second(loc(a, i)) == i
  }

  axiom length_nonneg {
    forall a: Array :: len(a) >= 0
  }
}

field val : Int

method setToArrayTwo(vals:Set[Ref]) returns (a:Array, n:Int)
    ensures forall i:Int :: 0 <= i && i< len(a) ==> acc(loc(a,i).val)
    ensures forall i:Int :: {i in vals} i in vals ==> let k == (n[i]) in 0 <= k && k < len(a) && loc(a,k).val == i

[viper-admin]

@alexanderjsummers commented on 2017-05-15 17:02

Note that the let expression doesn't type-check (but that's not the message which is generated)

[viper-admin]

@mschwerhoff commented on 2017-11-26 17:55

Stack trace:

Exception in thread "main" java.lang.AssertionError: assertion failed
	at scala.Predef$.assert(Predef.scala:156)
	at viper.silver.parser.TypeChecker.composeAndAdd(Resolver.scala:416)
	at viper.silver.parser.TypeChecker$$anonfun$unifySequenceWithSubstitutions$1$$anonfun$4$$anonfun$apply$3.apply(Resolver.scala:433)
	at viper.silver.parser.TypeChecker$$anonfun$unifySequenceWithSubstitutions$1$$anonfun$4$$anonfun$apply$3.apply(Resolver.scala:433)
	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.LinearSeqOptimized$class.foreach(LinearSeqOptimized.scala:73)
	at scala.collection.mutable.MutableList.foreach(MutableList.scala:30)
	at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
	at scala.collection.AbstractTraversable.map(Traversable.scala:104)
	at viper.silver.parser.TypeChecker$$anonfun$unifySequenceWithSubstitutions$1$$anonfun$4.apply(Resolver.scala:433)
	at viper.silver.parser.TypeChecker$$anonfun$unifySequenceWithSubstitutions$1$$anonfun$4.apply(Resolver.scala:433)
	...

[viper-admin]

@alexanderjsummers on 2018-10-15 15:36:

• changed the assignee from (none) to @Felalolf