CBMC
stack_depth.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Stack depth checks
4 
5 Author: Daniel Kroening, Michael Tautschnig
6 
7 Date: 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 
19 class goto_modelt;
20 class message_handlert;
21 
25 void 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
goto_modelt
Definition: goto_model.h:27
message_handlert
Definition: message.h:27
stack_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 ...
Definition: stack_depth.cpp:83