Exhaling field permissions fails after unfolding a predicate with permissions returned by `perm()`

[viper-admin]

Created by bitbucket user fhahn on 2015-12-07 16:48 Last updated on 2019-10-30 10:33

The following program fails when trying to exhale acc(x.Foo__a), even though the assertion perm(x.Foo__a) > none holds. Note that the predicate valid__Foo is unfolded with all permissions available for the predicate (perm(valid__Foo(x))). Carbon is able to verify the example when a permission variable (e.g. rd) is used instead.

#!scala

field Foo__a: Int
field Foo__b: Int

predicate valid__Foo(self: Ref) {
    acc(self.Foo__a)&&
    acc(self.Foo__b)
}

method test(rd: Perm)
    requires rd > none && rd < write
{
  var x: Ref
  x := new(Foo__a, Foo__b)
  x.Foo__a := 1
  x.Foo__b := 2

  fold acc(valid__Foo(x), rd)

  unfold acc(valid__Foo(x), perm(valid__Foo(x)))
  // unfold acc(valid__Foo(x), rd) // this works

  assert perm(x.Foo__b) > none

  exhale acc(x.Foo__a)
}

---

Attachments:

• carbon-exhale-perm.sil

[viper-admin]

Bitbucket user fhahn on 2015-12-07 16:50:

• edited the description

[viper-admin]

@fabiopakk commented on 2019-10-29 15:39

Fixing https://github.com/viperproject/carbon/issues/87: Remove 'fresh' statement. Remove Fresh node.

→ <<cset https://github.com/viperproject/carbon/commit/0496814db2d4756e0c997e715f4a2b823bdab57a>>

[viper-admin]

@fabiopakk commented on 2019-10-29 15:39

Fixing https://github.com/viperproject/carbon/issues/87: Remove 'fresh' statement. Remove Constrain node.

→ <<cset https://github.com/viperproject/carbon/commit/71579cb822a8e3cb7289808e6b8e2f8acbc970e9>>

[viper-admin]

@fabiopakk on 2019-10-29 15:39:

• changed state from new to resolved

[viper-admin]

@alexanderjsummers commented on 2019-10-29 15:42

Just a note: I don’t quite see how this issue relates to the fresh/constraining language features.

[viper-admin]

@fabiopakk commented on 2019-10-30 10:31

Apparently Bitbucket used the commit messages to infer that an issue should be closed, unfortunately by mistake. My commits refer to issue 87 in Silver, not in Carbon: https://github.com/viperproject/silver/issues/87. I’m reverting the state of this issue to opened.

[viper-admin]

@fabiopakk commented on 2019-10-30 10:33

This issue was mistakenly closed by Bitbucket. That commit that caused such issue refers to an issue with the same number (87) but on a different repository (Silver, as opposed to Carbon).

[viper-admin]

@fabiopakk on 2019-10-30 10:33:

• edited the description
• changed state from resolved to open