34 unsigned unwind_count,
38 const std::string &function_str =
id2string(function_id);
45 !class_id.
empty(),
"functions should have their defining class annotated");
48 size_t unwinds = class_type.
get_size_t(ID_java_enum_static_unwind);
49 if(unwinds != 0 && unwind_count < unwinds)
The type of an expression.
const std::string & id2string(const irep_idt &d)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
#define INVARIANT(CONDITION, REASON)
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...
const irep_idt & get(const irep_namet &name) const
typet type
Type of symbol.
Unwind loops in static initializers.
bool has_suffix(const std::string &s, const std::string &suffix)
std::size_t get_size_t(const irep_namet &name) const