If we forbid things like recursion (including mutual recursion), function pointers, dynamic dispatch, and unbounded use of alloca, doesn't it then follow from the call graph and the per-function worst-case stack-usage numbers (which the compiler presumably knows)? Is that mistaken, or is the difficulty in generalising this approach to where those restrictions are lifted?

I tried googling for how SPARK Ada provides assurances against exceeding stack-size limits, but I couldn't find a decent answer. I presume it does so, though.

edit: forgot about alloca

edit 2: Turns out the AdaCore folks have a tool specifically for static analysis of stack-space requirements of Ada/C/C++ code: https://www.adacore.com/gnatpro/toolsuite/gnatstack