30 static irep_idt reference_array_clone_id =
31 "java::array[reference].clone:()Ljava/lang/Object;";
34 const irep_idt ¤t_function = context.back().function_identifier;
36 if(context.size() >= 2 && current_function == reference_array_clone_id)
39 context.at(context.size() - 2).function_identifier;
40 if(
id2string(clone_caller).find(
".values:()[L") != std::string::npos)
46 return current_function;
69 unsigned unwind_count,
74 if(enum_function_id.
empty())
80 !class_id.
empty(),
"functions should have their defining class annotated");
83 size_t unwinds = class_type.
get_size_t(ID_java_enum_static_unwind);
84 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)
static irep_idt find_enum_function_on_stack(const goto_symex_statet::call_stackt &context)
Check if we may be in a function that loops over the cases of an enumeration (note we return a candid...
const irep_idt & get(const irep_namet &name) const
#define PRECONDITION(CONDITION)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
std::vector< framet > call_stackt
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
tvt java_enum_static_init_unwind_handler(const goto_symex_statet::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...