2 ms·
To clarify: it's not stack "space" that's at issue. It's the requirement that the lack of stack overflow at runtime be formally verified. If functions exist i
by ajross 2y ago
To clarify: it's not stack "space" that's at issue. It's the requirement that the lack of stack overflow at runtime be formally verified. If functions exist in a static call tree[1] you can do this with a little disassembly wizardry and a few hundred lines of python. If you allow them to call themselves recursively, or even to indirect through a function pointer, it becomes undecidable.
[1] There are some other related rules like "no alloca()".
- rcxdude 2y agoFunction pointers are possible to deal with, with varying levels of automation. You can detect when pointers to functions are taken, and tie them to call sides with type information or some manual work (I have a static analysis tool which allows function pointers for callbacks by linking functions passed into one function to the list of possible destinations for a given callsite). Recursion is harder but it's still possible in principle to prove a bound in a lot of cases, given a proof framework. Not something I'd encourage, though.