Ignore quantified fields/predicates in bodies of called methods

[marcoeilers]

The utility methods to determine which predicates or fields should be treated as quantified predicates or fields while verifying a given member walks through all members (transitively) referenced by said member. However, for methods that are called from the original method, it is not necessary to look into their bodies, since we only take into account their specification; thus, we should ignore any quantified permission assertions in the bodies of called methods.

[jcp19]

I only had minor comments and two questions.

I wonder if there is any historical reason for looking into all transitively referenced methods even when looking at method bodies.

Finally, is this change expected to have big performance implications? I would expect so, in particular, in scenarios like VerifiedSCION where we do have a lot of quantified permissions in handling slices.

[marcoeilers]

I don't know what the reason is, but I guess someone just forgot to exclude method bodies, I can't imagine that ever making sense.

And yes, this should speed up verification of some SCION methods (which call methods whose bodies use QPs for some field for which the caller itself never uses QPs) significantly; in fact, we found this issue after Gavin found some unexplicably bad performance when verifying two methods from the SCION code base together (each method individually verified in 20-40 seconds, both together basically did not terminate).