Stack depth checks. More...

#include "stack_depth.h"
#include <util/arith_tools.h>
#include <util/bitvector_types.h>
#include <util/c_types.h>
#include <goto-programs/goto_model.h>
#include <ansi-c/goto-conversion/goto_convert_functions.h>
#include <linking/static_lifetime_init.h>

Include dependency graph for stack_depth.cpp:

Go to the source code of this file.

Functions
static symbol_exprt	add_stack_depth_symbol (goto_modelt &goto_model, message_handlert &message_handler)

static void	stack_depth (goto_programt &goto_program, const symbol_exprt &symbol, const std::size_t i_depth, const exprt &max_depth)

void	stack_depth (goto_modelt &goto_model, const std::size_t depth, message_handlert &message_handler)
	Add assertions to all user-defined functions in `goto_model` that the call stack depth does not exceed `depth`. More...

Detailed Description

Stack depth checks.

Definition in file stack_depth.cpp.

Function Documentation

◆ add_stack_depth_symbol()

static symbol_exprt add_stack_depth_symbol	(	goto_modelt &	goto_model,
		message_handlert &	message_handler
	)

static

Definition at line 25 of file stack_depth.cpp.

◆ stack_depth() [1/2]

void stack_depth	(	goto_modelt &	goto_model,
		const std::size_t	depth,
		message_handlert &	message_handler
	)

Add assertions to all user-defined functions in goto_model that the call stack depth does not exceed depth.

Warnings are reported via message_handler.

Definition at line 83 of file stack_depth.cpp.

◆ stack_depth() [2/2]

static void stack_depth	(	goto_programt &	goto_program,
		const symbol_exprt &	symbol,
		const std::size_t	i_depth,
		const exprt &	max_depth
	)