Bound the stack a recursive tree walk may consume, so a pathologically deep expression or type yields a diagnostic instead of SIGSEGV (esbmc/esbmc#5048).
More...
template<class Tag>
class stack_budget_guardt< Tag >
Bound the stack a recursive tree walk may consume, so a pathologically deep expression or type yields a diagnostic instead of SIGSEGV (esbmc/esbmc#5048).
Counts bytes, not frames: a frame count tuned on one build is wrong on another – a Debug frame is several times an optimised one – whereas a byte budget holds whatever the frame costs.
Declare one instance at the top of the recursive function, then ask exceeded(). Reporting is left to the caller so the accounting can be exercised by a test without taking the process down with it.
Tag gives each walk its own base pointer and depth, so nested walks of different kinds do not measure each other. State is thread-local: several threads may be walking at once, on stacks that are nowhere near each other.
1.15.0