stack_budget.h File Reference

#include <cstddef>
#include <cstdint>

Include dependency graph for stack_budget.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

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

Variables
template<class Tag>
std::uintptr_t	stack_budget_guardt< Tag >::base = 0
template<class Tag>
unsigned	stack_budget_guardt< Tag >::depth = 0
constexpr std::ptrdiff_t	default_stack_budget = 384L * 1024 * 1024
	Default ceiling for a walk.

Variable Documentation

default_stack_budget

std::ptrdiff_t default_stack_budget = 384L * 1024 * 1024

constexpr

Default ceiling for a walk.

main() runs ESBMC on a 512 MiB stack (#6617); this leaves room to unwind and report rather than dying on the way out.

stack_budget_guardt< Tag >::base

template<class Tag>

std::uintptr_t stack_budget_guardt< Tag >::base = 0

thread_local

stack_budget_guardt< Tag >::depth

template<class Tag>

unsigned stack_budget_guardt< Tag >::depth = 0

thread_local