cprover
java_enum_static_init_unwind_handler.cpp File Reference

Unwind loops in static initializers. More...

Include dependency graph for java_enum_static_init_unwind_handler.cpp:

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...
 

Detailed Description

Unwind loops in static initializers.

Definition in file java_enum_static_init_unwind_handler.cpp.

Function Documentation

◆ java_enum_static_init_unwind_handler()

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.

Parameters
function_idfunction the loop is in
loop_numberordinal number of the loop (ignored)
unwind_countiteration count that is about to begin
[out]unwind_maxmay be set to an advisory (unenforced) maximum when we know the total iteration count
symbol_tableglobal symbol table
Returns
false if loop_id belongs to an enumeration's static initializer and unwind_count is <= the enumeration size, or unknown (defer / no decision) otherwise.

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().