CBMC
java_enum_static_init_unwind_handler.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Unwind loops in static initializers
4 
5 Author: Chris Smowton, chris.smowton@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H
13 #define CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H
14 
15 #include <util/threeval.h>
16 
17 class call_stackt;
18 class symbol_tablet;
19 
20 tvt java_enum_static_init_unwind_handler(
21  const call_stackt &context,
22  unsigned loop_number,
23  unsigned unwind_count,
24  unsigned &unwind_max,
25  const symbol_tablet &symbol_table);
26 
27 #endif // CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H
call_stackt
Definition: call_stack.h:15
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
tvt
Definition: threeval.h:20
java_enum_static_init_unwind_handler
tvt java_enum_static_init_unwind_handler(const call_stackt &context, unsigned loop_number, unsigned unwind_count, unsigned &unwind_max, const symbol_tablet &symbol_table)
Unwind handler that special-cases the clinit (static initializer) functions of enumeration classes,...
Definition: java_enum_static_init_unwind_handler.cpp:70