cbmc/java__enum__static__init__unwind__handler_8h_source.html

/*******************************************************************\


Module: Unwind loops in static initializers


Author: Chris Smowton, chris.smowton@diffblue.com


\*******************************************************************/


#ifndef CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H

#define CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H


#include <util/threeval.h>


class call_stackt;

class symbol_tablet;


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);


#endif // CPROVER_JAVA_BYTECODE_JAVA_ENUM_STATIC_INIT_UNWIND_HANDLER_H

ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562

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

threeval.h