The lifetime of obligations converted from unbounded to bounded is unknown

[viper-admin]

Created by @vakaras on 2016-04-13 16:37

In the following example method test1, acquire l produces an unbounded obligation which is then converted to a bounded one by the loop invariant. However, this bounded obligation does not have a method level lifetime and as a result, the call to do_release fails, because verifier cannot show that the obligation lifetime has decreased.

#!Chalice

class Lock {}
class A {

  method test1(l: Lock)
    requires l != null;
  {
    acquire l;
    while (true)
      invariant mustRelease(l, 1);
    {
      //:: UnexpectedOutput(call.precondition:assertion.false, /Chalice2Silver/issue/82/)
      call do_release(l);
      acquire l;
    }
  }

  method test2(l: Lock)
    requires l != null;
    requires mustRelease(l, 2);
  {
    while (true)
      invariant mustRelease(l, 1);
    {
      call do_release(l);
      acquire l;
    }
  }

  method do_release(l: Lock)
    requires l != null;
    requires mustRelease(l, 1);
  {
    release l;
  }

}