Translation of “forall c in collection” is wrong

[viper-admin]

Created by @vakaras on 2015-07-02 14:41

This Chalice example:

#!Chalice
  method test1(collection: seq<int>)
    requires |collection| >= 1
    requires (forall c in collection :: c == 0)
    ensures collection[0] == 0
  {
  }

is translated to:

#!Silver
method Statictest1$(this$_1: Ref, k$: Perm, collection: Seq[Int])
  requires this$_1 != null
  requires k$ > none
  requires write > k$
  requires |collection| >= 1
  requires (forall c: Int :: true && (c in collection) ==> (c == 0))
  ensures collection[0] == 0
{
}

and it should be translated to something like this:

#!Silver
method Statictest$(this$_2: Ref, k$_1: Perm, collection: Seq[Int])
  requires this$_2 != null
  requires k$_1 > none
  requires write > k$_1
  requires |collection| >= 1
  requires (forall i: Int :: true ==> (0 <= i) && (i < |collection|) ==> (collection[i] == 0))
  ensures collection[0] == 0
{
}

---

Attachments:

• internal-bug.chalice