Move shared-access predicate invariants to preconditions

[pawinkler]

Summary

This PR was extracted from #92 and is based on #106. It concerns moving the sharedPredicateAccessInvariant for method parameters from being expressed inside function bodies to being declared as requires clauses in method preconditions.

Shared-access predicate invariants ensure that an access to an object on the heap is permitted. Previously, these were only inhaled before the access occurred and it was not verified that the individual function actually has enough permissions to access the object. Implementing this change demonstrated that functions expecting a super type of the provided type did not have enough permissions to access it, leading to failures in the test cases.

Draft — the correctness of this implementation depends on the previous two PR requests.

Changes

• ProgramConverter: adds sharedPredicateAccessInvariant to method preconditions for each
  formal argument, so that the requires acc(Type_shared(param), wildcard) clause appears in
  the generated Viper method signature.
• FullNamedFunctionSignature.toViperFunction: removes the formalArgs.mapNotNull { it.sharedPredicateAccessInvariant() }
  that was previously prepended to pure-function preconditions; getPreconditions() is now
  used directly, which picks up the invariant from the method level.
• ControlFlow (FunctionExp.toViperMaybeStoringIn): removes the inline Stmt.Inhale of
  sharedPredicateAccessInvariant for each formal argument of an inline function body, which
  was a workaround that is no longer needed.

Remaining tasks

• Update all .fir.diag.txt golden files to reflect the new requires acc(...) lines in
  method preconditions.
• Verify that the moved permission does not introduce inconsistencies for callers that
  previously relied on the inhale.
• Decide whether uniquePredicateAccessInvariant should be moved to preconditions in the
  same way; currently only the shared predicate is moved.

Limitations

This strategy is not capable of handling casts to a subtype. Currently, when we explicitly or implicitly cast to a subtype, the permissions of this subtype are assumed. Our access predicate logic does not support an easy fix for this.