CBMC
Loading...
Searching...
No Matches
stack_depth.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Stack depth checks
4
5Author: Daniel Kroening, Michael Tautschnig
6
7Date: November 2011
8
9\*******************************************************************/
10
13
14#ifndef CPROVER_GOTO_INSTRUMENT_STACK_DEPTH_H
15#define CPROVER_GOTO_INSTRUMENT_STACK_DEPTH_H
16
17#include <cstddef>
18
19class goto_modelt;
21
25void stack_depth(
26 goto_modelt &goto_model,
27 const std::size_t depth,
28 message_handlert &message_handler);
29
30#endif // CPROVER_GOTO_INSTRUMENT_STACK_DEPTH_H
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 ...