Disallow use of wildcard in compound expressions

[mschwerhoff]

Viper currently allows wildcards in compound expressions, but semantics and practical relevance of such expressions are unclear. Viper should therefore reject such expressions, via suitable consistency checks. A few invalid examples are given below.

Related issues:

• ~~Silicon #569~~
• Carbon #85
• Carbon #169
• Carbon #376

Open question: How to avoid implicit compound expressions resulting from (un)folding acc(P(x), wildcard)? Reduce resulting expressions to just wildcard? See also Silver issue #206.

We should also check what the Viper tutorial says about wildcards, and update the tutorial, if necessary.

method test0() {
  var p: Perm := wildcard
  
  if (none == wildcard) {
    assert false
  }
}



field f: Ref

domain Frac {
  function box(p: Perm): Frac
  function unbox(q: Frac): Perm
}

method test1(b: Bool, x: Ref) {
  inhale acc(x.f, 2*wildcard)
  inhale acc(x.f, unbox(box(wildcard)))
  inhale acc(x.f, b ? wildcard : 1/2)
}



predicate P(x: Ref) {
  acc(x.f, 1/2)
}

method test2(x: Ref) {
  inhale acc(P(x), 1/3)
  unfold acc(P(x), wildcard) // ~~> wildcard * 1/2
}