search

viperproject / carbon

Verification-condition-generation-based verifier for the Viper intermediate verification language.
Mozilla Public License 2.0
30 stars 21 forks source link

`applying` not giving permission incompleteness #488

Open JonasAlaif opened 10 months ago

JonasAlaif commented 10 months ago

The following fails to verify in Carbon (with "There might be insufficient permission to access y.f" inside the applying) but succeeds in Silicon

field f: Int
method m() {
  var x: Ref, y: Ref
  inhale acc(x.f) && (acc(x.f) --* acc(y.f))
  assert (applying (acc(x.f) --* acc(y.f)) in y.f == 0) || true
}