46 auto &p=f->second.body;
47 for(
const auto &ins : p.instructions)
50 if(ins.is_backwards_goto())
52 size_t loop_id=ins.loop_number;
53 const std::string java_clinit=
"<clinit>:()V";
54 const std::string &fname=
id2string(ins.function);
55 size_t class_prefix_length=fname.find_last_of(
'.');
58 if(!(function_name.
mode==ID_java &&
has_suffix(fname, java_clinit)))
61 class_prefix_length!=std::string::npos &&
62 "could not identify class name");
63 const std::string &classname=fname.substr(0, class_prefix_length);
66 size_t unwinds=class_type.
get_size_t(ID_java_enum_static_unwind);
68 unwind_max=std::max(unwind_max, unwinds);
71 const std::string &
set=options.
get_option(
"unwindset");
76 id2string(ins.function)+
"."+std::to_string(loop_id)+
":"+
77 std::to_string(unwinds);
83 const std::string &vla_length=options.
get_option(
"java-max-vla-length");
84 if(!vla_length.empty())
87 if(max_vla_length<unwind_max)
88 throw "cannot unwind <clinit> due to insufficient max vla length";
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
const std::string & id2string(const irep_idt &d)
const symbol_tablet & symbol_table
irep_idt mode
Language mode.
void remove_static_init_loops(const symbol_tablet &symbol_table, const goto_functionst &goto_functions, optionst &options)
this is the entry point for the removal of loops in static initialization code of Java enums ...
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void unwind_enum_static(const goto_functionst &goto_functions, optionst &options)
unwind static initialization loops of Java enums as far as the enum has elements, thus flattening the...
const std::string get_option(const std::string &option) const
unsigned safe_string2unsigned(const std::string &str, int base)
typet type
Type of symbol.
remove_static_init_loopst(const symbol_tablet &_symbol_table)
bool has_suffix(const std::string &s, const std::string &suffix)
void set_option(const std::string &option, const bool value)
#define forall_goto_functions(it, functions)
Unwind loops in static initializers.
std::size_t get_size_t(const irep_namet &name) const
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.