Add support for explicit permissions in pre-/postconditions

[jesyspa]

Until we have uniqueness/for power users who want more explicit control, it would be great to be able to write the following to control permissions explicitly:

class X(var a: Any)
fun f(x: X) {
  precondition { acc(x, write) }
  ...
}

The main difficulty is how this will work with automated permission management, we want to disable any kind of predicate-based access or automatic in-/exhaling for a.x. Plus some design questions: Should we also disabling automation for other members of X? What about other base classes? Maybe require marking the whole function with @ManualPermissions?