[pron]

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).

[KsassPeuk]

Well, Frama-C is maintained thanks to public funding (Europe/France) and industrial users who use it for actual certification of systems. For example, Thales (Common Criteria EAL7), Airbus (DO-178C), EDF (ISO 60880). I don't know what you mean by professional tool if this is not professional ;)