GNATstack (https://www.adacore.com/gnatpro/toolsuite/gnatstack) does this (I think) using GCC stack-usage information, and propagating through static analysis. It has some limitations about procedure access types (function pointers) and returning dynamic-sized objects on the stack. But still, an interesting tool. For Ada and SPARK (that I know of), C/C++.
And to check for Stack Overflow in Ada at runtime compile with -fstack-check. The overhead is not so high and it saves from most of the stack corruption cases... Not all, especially if you're doing unsafe stuff...
BTW the GNAT Ada runtime comes with a nice tool to monitor dynamically maximum stack usage : https://www.adacore.com/gems/gem-93-gnat-dynamic-stack-analy... . To be used during tests and qualification, to get a somewhat clear picture.
And to check for Stack Overflow in Ada at runtime compile with -fstack-check. The overhead is not so high and it saves from most of the stack corruption cases... Not all, especially if you're doing unsafe stuff...