CBMC
|
Unwind loops in static initializers. More...
#include <util/threeval.h>
Go to the source code of this file.
Functions | |
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, and VALUES array cloning in their values() methods. More... | |
Unwind loops in static initializers.
Definition in file java_enum_static_init_unwind_handler.h.
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, and VALUES array cloning in their values() methods.
When java_bytecode_convert_classt has annotated them with a size of the enumeration type, this forces unwinding of any loop in the static initializer to at least that many iterations, with intent to permit population / copying of the enumeration's value array.
context | call stack when the loop back-edge was taken | |
loop_number | ordinal number of the loop (ignored) | |
unwind_count | iteration count that is about to begin | |
[out] | unwind_max | may be set to an advisory (unenforced) maximum when we know the total iteration count |
symbol_table | global symbol table |
Definition at line 70 of file java_enum_static_init_unwind_handler.cpp.