Missing assumptions that recursive predicate parameters must be different

[viper-admin]

Created by @vakaras on 2015-06-26 16:41 Last updated on 2015-06-29 10:23

The Chalice2Silver test chaliceSuite/general-tests/termination.chalice fails.

Related Chalice code fragment:

#!Chalice

class Node
{
  var val: int
  var next: Node

  predicate valid
  {
    acc(val) && acc(next) && (next!=null ==> next.valid)
  }

  function length():int
    requires valid
    ensures 0 <= result
  {
    unfolding valid in (next==null ? 1 : 1+next.length())
  }

  // ERROR: method does not terminate
  function t(): int
    requires rd*(valid)
  {
    unfolding rd*(valid) in t()
  }

  predicate p { p }

  // method precondition is equal to 'false', thus it is ok for the termination checks to not fail
  function t2(): int
    requires p
  {
    unfolding p in t()
  }
}

Error message:

[info] The following output occurred during testing, but should not have according to the test annotations:
[info]   [application.precondition:insufficient.permission] [application.precondition:insufficient.permission] Precondition of function Nodet$ might not hold. There might be insufficient permission to access Nodevalid$(this$_5). (termination.chalice,36:20) (AnnotationBasedTestSuite.scala:59)

---

Attachments:

• termination.chalice.sil

[viper-admin]

@vakaras commented on 2015-06-29 10:21

If recursive predicate contained itself with the same arguments, then its unrolling would be infinite, and, as a consequence, it is not possible to construct such predicate. Therefore, predicate p in this case is equivalent to false. However, Silicon does not have needed assumptions and cannot show that.

[viper-admin]

@vakaras on 2015-06-29 10:23:

• edited the title