feat: Allow functions to depend on allocation set

[RustanLeino]

This PR introduces a reads ** clause on functions. It allows a function to depend on the allocation set, for example by explicitly using allocated(_) or using an unbounded quantification over objects. Such a function gets no frame axiom at all, which means that any change of the heap (including a call to a method with an empty modifies clause, since such a method is still allowed to change the allocation set) may change the value returned by the function.

The PR also updates the reference manual and FAQ about this point.

In addition, this PR

• allows the by method part of a function to use the function naked (that is, without applying the function to arguments)
• makes the FAQ format a little more consistent across questions
• fixes a typo in a comment in the standard library
• updates the FAQ to mention the availability of datatypes that extend traits

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[volodeyka]

Great! We really need this feature to quantify over classes (for example, variables are defined as classes) in B3 soundness proof. Thanks!