CBMC
java_enum_static_init_unwind_handler.h File Reference

Unwind loops in static initializers. More...

#include <util/threeval.h>
+ Include dependency graph for java_enum_static_init_unwind_handler.h:
+ This graph shows which files directly or indirectly include this file:

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

Detailed Description

Unwind loops in static initializers.

Definition in file java_enum_static_init_unwind_handler.h.

Function Documentation

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

Parameters
contextcall stack when the loop back-edge was taken
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 70 of file java_enum_static_init_unwind_handler.cpp.