Search code examples
viper-lang

Does multiplying a wildcard in viper mean anything?

A bug in VerCors generated some silver that looks like:

field f: Int

method test(n: Int, x: Ref)
requires n == 100
requires acc(x.f, wildcard * n)    
{}

Viper seems to accept this, but I don't understand what it would mean, if anything.

Solution

  • Intuitively, it means that the callee obtains a tiny (but non-zero) permission amount — times n. In effect, this should be no different from just obtaining the tiny amount (i.e. acc(x.f, wildcard)), although one can maybe engineer contrived situations, in probably involving perm, in which it makes a difference.

    Bottom line: The example is indeed somewhat confusing and the semantics not totally obvious, but everything is well defined.