A new annotation should have the semantics of both @EnsuresCalledMethods and @EnsuresCalledMethodsOnException

[kelloggm]

          Agreed that we need such an annotation and that we can do it in a follow-up to this PR.  I would strongly prefer to have at least an alias for the annotation that has fewer characters to type than `@EnsuresCalledMethodsOnAllPaths`; maybe `@AlwaysCalls`?  But we can discuss that as part of the follow-up.

Originally posted by @msridhar in #6271 (comment)

[kelloggm]

Here are some thoughts about how this should be named (summarizing discussion with @msridhar, @Nargeshdb, and @mernst over a call):

• Within the Called Methods Checker context, it's probably better if the new annotation has a name that starts with @EnsuresCalledMethods..., to maintain the parallel structure
• to keep consistency with the rest of the CF, it's important that @EnsuresCalledMethods's semantics continue to mean "ensures the postcondition on regular exit paths". Naming the new annotation @EnsuresCalledMethods (and creating a new @EnsuresCalledMethodsOnRegularExit or similar annotation) is probably not an option for this reason.
• In the RLC, we expect that the new annotation will be used commonly for destructors and finalizers, so it would be nice if it had a short, easy to remember name. One option is @AlwaysCalls. However, this doesn't have parallel structure with the @Ensures... annotations. I suggested we could create both an annotation with this name (in the RLC namespace) and one with an @Ensures... name (in the Called Methods namespace), and make them aliases. This is okay, but CMC users might be confused about why they can't use the shorter alias.
• we expect that @EnsuresCalledMethods (on regular exit) will be more common/useful for users of the CMC who are not using the RLC, but that the "on all paths" version will be more common/useful for RLC users. This makes it difficult to say which annotation should have the "shorter" name, since they'll both be common in different contexts. This is a reason to have multiple aliases.

[kelloggm]

If I forgot anything please feel free to add on!