silicon

silicon copied to clipboard

I think the following program should verify. Find out, why it doesn't.

field val: Int

function req_wand(a: Ref): Int
  requires acc(a.val) --* acc(a.val)

method test_wand_framing_2(a: Ref) {
  inhale acc(a.val)
  package acc(a.val) --* acc(a.val) // If this were an inhale, #304 might apply
  inhale req_wand(a) == 0

  apply acc(a.val) --* acc(a.val)
  package acc(a.val) --* acc(a.val)

  assert req_wand(a) == 0
}

Added corresponding regression test with an additional variant that should definitely verify.

Just for reference, without further investigation: This verifies in my fork with semantic heap snapshots.