Non-aliasing assumptions from unfolding predicates

[viper-admin]

Created by @mschwerhoff on 2013-07-31 08:48 Last updated on 2019-11-16 14:58

Additional non-aliasing assumptions could be generated when unfolding permissions, as illustrated by the following program:

field next: Ref

predicate valid(this: Ref) {
  acc(this.next, wildcard) &&
  (((this.next) != (null)) ==> acc(valid(this.next), wildcard))
}

method testNestingUnfold(this: Ref)
  requires acc(valid(this), wildcard)
{
  unfold acc(valid(this), wildcard)
  assert ((this) != (this.next))

  if (((this.next) != (null))) {
    unfold acc(valid(this.next), wildcard)
    assert ((this.next) != (this.next.next))
    assert ((this) != (this.next.next))
  }
}

This is currently not done in Silicon.

[viper-admin]

@alexanderjsummers on 2019-08-28 09:34:

• edited the description

[viper-admin]

@alexanderjsummers commented on 2019-08-28 09:35

The issue was fixed, but the code wasn't valid Viper code

[viper-admin]

@alexanderjsummers on 2019-08-28 09:35:

• changed state from new to resolved

[viper-admin]

@mschwerhoff commented on 2019-11-16 14:58

This issue wasn't actually resolved, as can be seen when replacing each wildcard by 1/2 or write. It is merely a coincidence that the program as-is now verifies.

[viper-admin]

@mschwerhoff on 2019-11-16 14:58:

• changed state from resolved to open