cprover
|
Unwind loops in static initializers. More...
Go to the source code of this file.
Functions | |
tvt | java_enum_static_init_unwind_handler (const irep_idt &function_id, 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. More... | |
Unwind loops in static initializers.
Definition in file java_enum_static_init_unwind_handler.h.
tvt java_enum_static_init_unwind_handler | ( | const irep_idt & | function_id, |
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.
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 of the enumeration's value array.
function_id | function the loop is in | |
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 31 of file java_enum_static_init_unwind_handler.cpp.
References dstringt::empty(), irept::get(), irept::get_size_t(), has_suffix(), id2string(), INVARIANT, symbol_table_baset::lookup_ref(), symbolt::type, and tvt::unknown().
Referenced by jbmc_parse_optionst::doit().