So the annotations for such tools are pre/post conditions for certain properties (say, pointer validity, ownership). Like types, function annotations can sometimes be inferred, or they may need to be explicit. Once that information is known about a function, there's no need for the tool to look inside it again when analysing callers.

If you want to get a sense of what that may look like, see https://www.frama-c.com (which is a community project, so maybe not as smooth and polished like more professional tools).