cprover
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 
16 
17 #include <util/symbol_table.h>
18 #include <util/threeval.h>
19 
21  const goto_symex_statet::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
Symbolic Execution.
Definition: threeval.h:19
The symbol table.
Definition: symbol_table.h:19
tvt java_enum_static_init_unwind_handler(const goto_symex_statet::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...
Author: Diffblue Ltd.
std::vector< framet > call_stackt