From 318ab8612592da2211b62a67b97fb8d88b29d74b Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 10 Apr 2017 17:02:51 +0100 Subject: [PATCH 1/4] Improve `class_typet`'s base description This defines an exprt subclass representing a base class instead of using a bare exprt, and enforces proper types when returning the base list. It's the same shape as the existing exprt so old code doesn't need adjusting, it just makes client code neater. --- src/cegis/cegis-util/type_helper.cpp | 6 ++--- src/util/std_types.h | 33 ++++++++++++++++++---------- 2 files changed, 24 insertions(+), 15 deletions(-) diff --git a/src/cegis/cegis-util/type_helper.cpp b/src/cegis/cegis-util/type_helper.cpp index b20ea9d08e6..e60b597b3a0 100644 --- a/src/cegis/cegis-util/type_helper.cpp +++ b/src/cegis/cegis-util/type_helper.cpp @@ -34,10 +34,10 @@ bool instanceof(const typet &lhs, const typet &rhs, const namespacet &ns) if (type_eq(lhs, rhs, ns)) return true; assert(ID_class == lhs.id()); const class_typet &lhs_class=to_class_type(lhs); - const irept::subt &bases=lhs_class.bases(); - for (const irept &base : bases) + const class_typet::basest &bases=lhs_class.bases(); + for(const exprt &base : bases) { - const typet &type=static_cast(base.find(ID_type)); + const typet &type=base.type(); if (instanceof(ns.follow(type), rhs, ns)) return true; } return false; diff --git a/src/util/std_types.h b/src/util/std_types.h index 02f4a3981a1..4b3ec6e698e 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -361,31 +361,40 @@ class class_typet:public struct_typet return is_class()?ID_private:ID_public; } - const irept::subt &bases() const + class baset:public exprt { - return find(ID_bases).get_sub(); + public: + baset():exprt(ID_base) + { + } + + explicit baset(const typet &base):exprt(ID_base, base) + { + } + }; + + typedef std::vector basest; + + const basest &bases() const + { + return (const basest &)find(ID_bases).get_sub(); } - irept::subt &bases() + basest &bases() { - return add(ID_bases).get_sub(); + return (basest &)add(ID_bases).get_sub(); } void add_base(const typet &base) { - bases().push_back(exprt(ID_base, base)); + bases().push_back(baset(base)); } bool has_base(const irep_idt &id) const { - const irept::subt &b=bases(); - - forall_irep(it, b) + for(const auto &b : bases()) { - assert(it->id()==ID_base); - const irept &type=it->find(ID_type); - assert(type.id()==ID_symbol); - if(type.get(ID_identifier)==id) + if(to_symbol_type(b.type()).get(ID_identifier)==id) return true; } From 668f30f0e31a0e2e96745084d52bf670acc02cf7 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 10 Apr 2017 17:04:36 +0100 Subject: [PATCH 2/4] Always convert methods in two phases, even in eager mode Previously in lazy mode we first converted all the method prototypes, then later populated bodies, while in eager mode bodies were populated as we went. Now we always use the former method, so eager mode is like lazy mode except we then populate every method regardless of reachability. This makes the process more uniform, and as a useful side-effect means that the symbol table is populated by the time method conversion happens, so we can check for static initialisers' existence or otherwise. --- .../java_bytecode_convert_class.cpp | 16 +--------------- src/java_bytecode/java_bytecode_language.cpp | 14 ++++++++++++++ 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 2926da79fc3..0990027e0a0 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -171,21 +171,7 @@ void java_bytecode_convert_classt::convert(const classt &c) method_identifier, method, symbol_table); - if(lazy_methods_mode==LAZY_METHODS_MODE_EAGER) - { - // Upgrade to a fully-realized symbol now: - java_bytecode_convert_method( - *class_symbol, - method, - symbol_table, - get_message_handler(), - max_array_length); - } - else - { - // Wait for our caller to decide what needs elaborating. - lazy_methods[method_identifier]=std::make_pair(class_symbol, &method); - } + lazy_methods[method_identifier]=std::make_pair(class_symbol, &method); } // is this a root class? diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 43e6fac96c0..444208f0c87 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -542,6 +542,20 @@ bool java_bytecode_languaget::typecheck( if(do_ci_lazy_method_conversion(symbol_table, lazy_methods)) return true; } + else if(lazy_methods_mode==LAZY_METHODS_MODE_EAGER) + { + // Simply elaborate all methods symbols now. + for(const auto &method_sig : lazy_methods) + { + java_bytecode_convert_method( + *method_sig.second.first, + *method_sig.second.second, + symbol_table, + get_message_handler(), + max_user_array_length); + } + } + // Otherwise our caller is in charge of elaborating methods on demand. // now typecheck all if(java_bytecode_typecheck( From 85b1e4f4fa066876a37fa90f271cd37594982b92 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 10 Apr 2017 17:07:10 +0100 Subject: [PATCH 3/4] Invoke static initializers on demand Previously these were run from CPROVER_init; now they are run on demand, using the same rules as the JVM (in brief, when `new` is called, or a static field accessed, or a static method called). This means that a faulting static initializer no longer blocks all coverage, instead blocking only paths that would necessarily call the problematic initializer, and initializers are called in the correct order, which they sometimes depend upon (e.g. a class initializer assuming an enumeration initializer has run before it uses the `.values()` method) For details, see http://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4 This commit also amends the covered1 test, whose precise results I think are still correct, but are perturbed by this change. --- regression/cbmc-java/covered1/test.desc | 3 +- .../java_bytecode_convert_method.cpp | 206 +++++++++++++++++- .../java_bytecode_convert_method_class.h | 6 + src/java_bytecode/java_entry_point.cpp | 57 ----- 4 files changed, 211 insertions(+), 61 deletions(-) diff --git a/regression/cbmc-java/covered1/test.desc b/regression/cbmc-java/covered1/test.desc index 32af766bdb7..6f78ed37e63 100644 --- a/regression/cbmc-java/covered1/test.desc +++ b/regression/cbmc-java/covered1/test.desc @@ -11,9 +11,8 @@ covered1.class .*\"coveredLines\": \"28\",$ .*\"coveredLines\": \"28\",$ .*\"coveredLines\": \"29\",$ -.*\"coveredLines\": \"9,18\",$ .*\"coveredLines\": \"18\",$ .*\"coveredLines\": \"18\",$ -.*\"coveredLines\": \"18,35\",$ +.*\"coveredLines\": \"35\",$ -- ^warning: ignoring diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index 4888810bd83..8d7d63c3c71 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -911,6 +911,174 @@ void java_bytecode_convert_methodt::check_static_field_stub( /*******************************************************************\ +Function: java_bytecode_convert_methodt::class_needs_clinit + + Inputs: classname: Class name + + Outputs: Returns true if the given class or one of its parents + has a static initializer + + Purpose: Determine whether a `new` or static access against `classname` + should be prefixed with a static initialization check. + +\*******************************************************************/ + +bool java_bytecode_convert_methodt::class_needs_clinit( + const irep_idt &classname) +{ + auto findit_any=any_superclass_has_clinit_method.insert({classname, false}); + if(!findit_any.second) + return findit_any.first->second; + + auto findit_here=class_has_clinit_method.insert({classname, false}); + if(findit_here.second) + { + const irep_idt &clinit_name=id2string(classname)+".:()V"; + findit_here.first->second=symbol_table.symbols.count(clinit_name); + } + if(findit_here.first->second) + { + findit_any.first->second=true; + return true; + } + auto findit_symbol=symbol_table.symbols.find(classname); + // Stub class? + if(findit_symbol==symbol_table.symbols.end()) + { + warning() << "SKIPPED: " << classname << eom; + return false; + } + const symbolt &class_symbol=symbol_table.lookup(classname); + for(const auto &base : to_class_type(class_symbol.type).bases()) + { + if(class_needs_clinit(to_symbol_type(base.type()).get_identifier())) + { + findit_any.first->second=true; + return true; + } + } + return false; +} + +/*******************************************************************\ + +Function: java_bytecode_convert_methodt::get_or_create_clinit_wrapper + + Inputs: classname: Class name + + Outputs: Returns a symbol_exprt pointing to the given class' clinit + wrapper if one is required, or nil otherwise. + + Purpose: Create a ::clinit_wrapper the first time a static initializer + might be called. The wrapper method checks whether static init + has already taken place, calls the actual method if + not, and initializes super-classes and interfaces. + +\*******************************************************************/ + +exprt java_bytecode_convert_methodt::get_or_create_clinit_wrapper( + const irep_idt &classname) +{ + if(!class_needs_clinit(classname)) + return static_cast(get_nil_irep()); + + const irep_idt &clinit_wrapper_name= + id2string(classname)+"::clinit_wrapper"; + auto findit=symbol_table.symbols.find(clinit_wrapper_name); + if(findit!=symbol_table.symbols.end()) + return findit->second.symbol_expr(); + + // Create the wrapper now: + const irep_idt &already_run_name= + id2string(classname)+"::clinit_already_run"; + symbolt already_run_symbol; + already_run_symbol.name=already_run_name; + already_run_symbol.pretty_name=already_run_name; + already_run_symbol.base_name="clinit_already_run"; + already_run_symbol.type=bool_typet(); + already_run_symbol.value=false_exprt(); + already_run_symbol.is_lvalue=true; + already_run_symbol.is_state_var=true; + already_run_symbol.is_static_lifetime=true; + already_run_symbol.mode=ID_java; + symbol_table.add(already_run_symbol); + + equal_exprt check_already_run( + already_run_symbol.symbol_expr(), + false_exprt()); + + code_ifthenelset wrapper_body; + wrapper_body.cond()=check_already_run; + code_blockt init_body; + // Note already-run is set *before* calling clinit, in order to prevent + // recursion in clinit methods. + code_assignt set_already_run(already_run_symbol.symbol_expr(), true_exprt()); + init_body.move_to_operands(set_already_run); + const irep_idt &real_clinit_name=id2string(classname)+".:()V"; + const symbolt &class_symbol=symbol_table.lookup(classname); + + auto findsymit=symbol_table.symbols.find(real_clinit_name); + if(findsymit!=symbol_table.symbols.end()) + { + code_function_callt call_real_init; + call_real_init.function()=findsymit->second.symbol_expr(); + init_body.move_to_operands(call_real_init); + } + + for(const auto &base : to_class_type(class_symbol.type).bases()) + { + const auto base_name=to_symbol_type(base.type()).get_identifier(); + exprt base_init_routine=get_or_create_clinit_wrapper(base_name); + if(base_init_routine.is_nil()) + continue; + code_function_callt call_base; + call_base.function()=base_init_routine; + init_body.move_to_operands(call_base); + } + + wrapper_body.then_case()=init_body; + + symbolt wrapper_method_symbol; + code_typet wrapper_method_type; + wrapper_method_type.return_type()=void_typet(); + wrapper_method_symbol.name=clinit_wrapper_name; + wrapper_method_symbol.pretty_name=clinit_wrapper_name; + wrapper_method_symbol.base_name="clinit_wrapper"; + wrapper_method_symbol.type=wrapper_method_type; + wrapper_method_symbol.value=wrapper_body; + wrapper_method_symbol.mode=ID_java; + symbol_table.add(wrapper_method_symbol); + return wrapper_method_symbol.symbol_expr(); +} + +/*******************************************************************\ + +Function: java_bytecode_convert_methodt::get_clinit_call + + Inputs: classname: Class name + + Outputs: Returns a function call to the given class' static initializer + wrapper if one is needed, or a skip instruction otherwise. + + Purpose: Each static access to classname should be prefixed with a check + for necessary static init; this returns a call implementing + that check. + +\*******************************************************************/ + +codet java_bytecode_convert_methodt::get_clinit_call( + const irep_idt &classname) +{ + exprt callee=get_or_create_clinit_wrapper(classname); + if(callee.is_nil()) + return code_skipt(); + code_function_callt ret; + ret.function()=callee; + return ret; +} + +/*******************************************************************\ + Function: java_bytecode_convert_methodt::convert_instructions Inputs: @@ -1378,6 +1546,18 @@ codet java_bytecode_convert_methodt::convert_instructions( call.function().add_source_location()=loc; c=call; + + if(!use_this) + { + codet clinit_call=get_clinit_call(arg0.get(ID_C_class)); + if(clinit_call.get_statement()!=ID_skip) + { + code_blockt ret_block; + ret_block.move_to_operands(clinit_call); + ret_block.move_to_operands(c); + c=std::move(ret_block); + } + } } else if(statement=="return") { @@ -1916,9 +2096,14 @@ codet java_bytecode_convert_methodt::convert_instructions( } results[0]=java_bytecode_promotion(symbol_expr); - // set $assertionDisabled to false - if(field_name.find("$assertionsDisabled")!=std::string::npos) + codet clinit_call=get_clinit_call(arg0.get_string(ID_class)); + if(clinit_call.get_statement()!=ID_skip) + c=clinit_call; + else if(field_name.find("$assertionsDisabled")!=std::string::npos) + { + // set $assertionDisabled to false c=code_assignt(symbol_expr, false_exprt()); + } } else if(statement=="putfield") { @@ -1937,6 +2122,14 @@ codet java_bytecode_convert_methodt::convert_instructions( to_symbol_type(arg0.type()).get_identifier()); } c=code_assignt(symbol_expr, op[0]); + codet clinit_call=get_clinit_call(arg0.get_string(ID_class)); + if(clinit_call.get_statement()!=ID_skip) + { + code_blockt ret_block; + ret_block.move_to_operands(clinit_call); + ret_block.move_to_operands(c); + c=std::move(ret_block); + } } else if(statement==patternt("?2?")) // i2c etc. { @@ -1955,6 +2148,15 @@ codet java_bytecode_convert_methodt::convert_instructions( const exprt tmp=tmp_variable("new", ref_type); c=code_assignt(tmp, java_new_expr); + codet clinit_call= + get_clinit_call(to_symbol_type(arg0.type()).get_identifier()); + if(clinit_call.get_statement()!=ID_skip) + { + code_blockt ret_block; + ret_block.move_to_operands(clinit_call); + ret_block.move_to_operands(c); + c=std::move(ret_block); + } results[0]=tmp; } else if(statement=="newarray" || diff --git a/src/java_bytecode/java_bytecode_convert_method_class.h b/src/java_bytecode/java_bytecode_convert_method_class.h index d260b82bbc8..75cfacd222e 100644 --- a/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/src/java_bytecode/java_bytecode_convert_method_class.h @@ -94,6 +94,8 @@ class java_bytecode_convert_methodt:public messaget expanding_vectort variables; std::set used_local_names; bool method_has_this; + std::map class_has_clinit_method; + std::map any_superclass_has_clinit_method; typedef enum instruction_sizet { @@ -221,6 +223,10 @@ class java_bytecode_convert_methodt:public messaget void check_static_field_stub( const symbol_exprt &se, const irep_idt &basename); + + bool class_needs_clinit(const irep_idt &classname); + exprt get_or_create_clinit_wrapper(const irep_idt &classname); + codet get_clinit_call(const irep_idt &classname); }; #endif diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 3e4de0cdea5..edac8f5cbb3 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -98,19 +98,6 @@ Function: java_static_lifetime_init \*******************************************************************/ -struct static_initializer_callt -{ - symbol_exprt initializer_symbol; - bool is_enum; -}; - -static bool static_initializer_call_enum_lt( - const static_initializer_callt &a, - const static_initializer_callt &b) -{ - return a.is_enum && !b.is_enum; -} - bool java_static_lifetime_init( symbol_tablet &symbol_table, const source_locationt &source_location, @@ -169,50 +156,6 @@ bool java_static_lifetime_init( } } - // we now need to run all the methods - - std::vector clinits; - - for(symbol_tablet::symbolst::const_iterator - it=symbol_table.symbols.begin(); - it!=symbol_table.symbols.end(); - it++) - { - if(it->second.base_name=="" && - it->second.type.id()==ID_code && - it->second.mode==ID_java) - { - const irep_idt symbol_name= - it->second.symbol_expr().get_identifier(); - const std::string &symbol_str=id2string(symbol_name); - const std::string suffix(".:()V"); - assert(has_suffix(symbol_str, suffix)); - const std::string class_symbol_name= - symbol_str.substr(0, symbol_str.size()-suffix.size()); - const symbolt &class_symbol=symbol_table.lookup(class_symbol_name); - clinits.push_back( - { - it->second.symbol_expr(), - class_symbol.type.get_bool(ID_enumeration) - }); - } - } - - // Call enumeration initialisers before anything else. - // Really we should be calling them the first time they're referenced, - // as acccording to the JVM spec, but this ought to do the trick for - // most cases with much less effort. - std::sort(clinits.begin(), clinits.end(), static_initializer_call_enum_lt); - - for(const auto &clinit : clinits) - { - code_function_callt function_call; - function_call.lhs()=nil_exprt(); - function_call.function()=clinit.initializer_symbol; - function_call.add_source_location()=source_location; - code_block.add(function_call); - } - return false; } From c631419022412f5e6dc210a24037e896bbba14d2 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 10 Apr 2017 17:44:36 +0100 Subject: [PATCH 4/4] Add tests for static initialization order These test mutually dependent static initializers, where the order that fields are referenced in the source program dictate the results of initialization. --- regression/cbmc-java/static_init1/A.class | Bin 0 -> 314 bytes regression/cbmc-java/static_init1/B.class | Bin 0 -> 314 bytes .../cbmc-java/static_init1/static_init.class | Bin 0 -> 588 bytes .../cbmc-java/static_init1/static_init.java | 32 ++++++++++++++++++ regression/cbmc-java/static_init1/test.desc | 8 +++++ regression/cbmc-java/static_init2/A.class | Bin 0 -> 314 bytes regression/cbmc-java/static_init2/B.class | Bin 0 -> 314 bytes .../cbmc-java/static_init2/static_init.class | Bin 0 -> 587 bytes .../cbmc-java/static_init2/static_init.java | 32 ++++++++++++++++++ regression/cbmc-java/static_init2/test.desc | 8 +++++ 10 files changed, 80 insertions(+) create mode 100644 regression/cbmc-java/static_init1/A.class create mode 100644 regression/cbmc-java/static_init1/B.class create mode 100644 regression/cbmc-java/static_init1/static_init.class create mode 100644 regression/cbmc-java/static_init1/static_init.java create mode 100644 regression/cbmc-java/static_init1/test.desc create mode 100644 regression/cbmc-java/static_init2/A.class create mode 100644 regression/cbmc-java/static_init2/B.class create mode 100644 regression/cbmc-java/static_init2/static_init.class create mode 100644 regression/cbmc-java/static_init2/static_init.java create mode 100644 regression/cbmc-java/static_init2/test.desc diff --git a/regression/cbmc-java/static_init1/A.class b/regression/cbmc-java/static_init1/A.class new file mode 100644 index 0000000000000000000000000000000000000000..cc4eabe977212306c26ea2916185d25d0d4bfa6c GIT binary patch literal 314 zcmYL@%}T>i5QWbqY5r}~+NvADr9aSaToyqEK`3=$aVt0RBDcg8YAX6z+J)f42k@c9 zbA#w&?#z61&fNL>{`drNjGY)hx)ECFMc72&R{a2j09yiiW?V8}1pe4mralq4`v*4y z?|gBm1)Yhh^mO%*>*Y-4B}q6g%3o!Cy;v;^ePJxm9&1&b;?~ZFbM>TB#7I&E2m@@V zh!FClQwr^HRI2KJbd}F_Q4^nGk9YaJ*rAXXR*|(d1a=byDZ5=}VQwA1Lta@3Hu(At kOlWBTNsk%^B;Fd%8{9R#e?uECZ5cdtxxGhehrNUB2bL%*e*gdg literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/static_init1/B.class b/regression/cbmc-java/static_init1/B.class new file mode 100644 index 0000000000000000000000000000000000000000..448af9210504502e94f0a39aa6b8e6fe4f08eec5 GIT binary patch literal 314 zcmYL@%Sr=55JhjzWS$w5_=;2!iNBaVtGzBOS&G#EF>CO0p1K_yK-Y z$n8;dQPowq&aJNR#pf4*6Ku!uu^M3w>k+)4v=Lx4KwBX1j4Q@O;P*{o%2R=R*m)4t zE{0E9(7ZNEy_Tvp*`u9x2kK2Fh*1x)l^{Tv zAVSEG&I#IKFIUBL?=~IitfYK~10Lt|Vuv7kR*|(-3hX8b5_Wrhg|Bz?0hzK8tT6kP l*ruWJhaOiNP@ln>!}aE<{Tmu^Y1^T3m)rM=HrYF9EdiV)Dy{$k literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/static_init1/static_init.class b/regression/cbmc-java/static_init1/static_init.class new file mode 100644 index 0000000000000000000000000000000000000000..92cc80f9170adfd67ea86c9d2c4ced1bf3fde393 GIT binary patch literal 588 zcmYk3PjAye5XFD%*xA@|Y0^R)paoh2ZG%KFJywWPKtke=P!STnAjh%LmefJEgW#+5 zLT{Wg5|u!LJ0A)$Yubdv%y?(sym>SJ{pb5nV2fTrlSLn&j?YCd`CR_zmh5v$vmBsV z)LaR;$~Dc3V!j*Yd6E@ol;-zM9`%RGK%w>(^=*@y;*O%WzVTAw?v4hDV)n5~lc(du zev-YgU@06%CRNPr6;b^5N%ZbC-Pn$Yrv$;?Xq?5#Lu28syod@DzqYm82hsZ|Hh0csKFG3BrfB}hqge}CXG7Sh4bS=qNnFS-J7OQi z9*Nx(`zTvXVY@>)fMQ{gOdu|V45>s3-o^V|gb97if}tHe2Ct)%82(~? literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/static_init1/static_init.java b/regression/cbmc-java/static_init1/static_init.java new file mode 100644 index 00000000000..778b6926fcc --- /dev/null +++ b/regression/cbmc-java/static_init1/static_init.java @@ -0,0 +1,32 @@ +public class static_init { + + // A should be initialised first, then B will begin init + // after A.x is set. + public static void main() { + assert(A.x == 1 && B.x == 1 && B.y == 2 && A.y == 2); + } + +} + +class A { + + public static int x; + public static int y; + static { + x = 1; + y = B.y; + } + +} + +class B { + + public static int x; + public static int y; + static { + x = A.x; + y = 2; + + } + +} diff --git a/regression/cbmc-java/static_init1/test.desc b/regression/cbmc-java/static_init1/test.desc new file mode 100644 index 00000000000..30868289dae --- /dev/null +++ b/regression/cbmc-java/static_init1/test.desc @@ -0,0 +1,8 @@ +CORE +static_init.class + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/static_init2/A.class b/regression/cbmc-java/static_init2/A.class new file mode 100644 index 0000000000000000000000000000000000000000..cc4eabe977212306c26ea2916185d25d0d4bfa6c GIT binary patch literal 314 zcmYL@%}T>i5QWbqY5r}~+NvADr9aSaToyqEK`3=$aVt0RBDcg8YAX6z+J)f42k@c9 zbA#w&?#z61&fNL>{`drNjGY)hx)ECFMc72&R{a2j09yiiW?V8}1pe4mralq4`v*4y z?|gBm1)Yhh^mO%*>*Y-4B}q6g%3o!Cy;v;^ePJxm9&1&b;?~ZFbM>TB#7I&E2m@@V zh!FClQwr^HRI2KJbd}F_Q4^nGk9YaJ*rAXXR*|(d1a=byDZ5=}VQwA1Lta@3Hu(At kOlWBTNsk%^B;Fd%8{9R#e?uECZ5cdtxxGhehrNUB2bL%*e*gdg literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/static_init2/B.class b/regression/cbmc-java/static_init2/B.class new file mode 100644 index 0000000000000000000000000000000000000000..448af9210504502e94f0a39aa6b8e6fe4f08eec5 GIT binary patch literal 314 zcmYL@%Sr=55JhjzWS$w5_=;2!iNBaVtGzBOS&G#EF>CO0p1K_yK-Y z$n8;dQPowq&aJNR#pf4*6Ku!uu^M3w>k+)4v=Lx4KwBX1j4Q@O;P*{o%2R=R*m)4t zE{0E9(7ZNEy_Tvp*`u9x2kK2Fh*1x)l^{Tv zAVSEG&I#IKFIUBL?=~IitfYK~10Lt|Vuv7kR*|(-3hX8b5_Wrhg|Bz?0hzK8tT6kP l*ruWJhaOiNP@ln>!}aE<{Tmu^Y1^T3m)rM=HrYF9EdiV)Dy{$k literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/static_init2/static_init.class b/regression/cbmc-java/static_init2/static_init.class new file mode 100644 index 0000000000000000000000000000000000000000..6a0da38e0293aaadf5d826f54768613ea7e9b6e6 GIT binary patch literal 587 zcmYk3PjAye5XFD%IN8{7Y1%>)XbXgf(&RudJywWPKtkf5RD?t?$Z=McOX?uoLGV%N zsW;9TiAo^BoezbWwc3Qk%)!tTF(X9Ds zTAJ%VH@KE4?QQL`=IKQW;Z1!F&+`aM8DCVEWiFrOb z9+>o%1xw;Mj1$G&ejY~eo`vtv!}XnLbWY&!k0)tl9>*5m%P)ur)^}Md?E>%{(z3`v>`iI&9)UPw+hPY7T=WDnw(0` zYX1!N)dE=%Un_%3iWjHQmpGDvet~nsMnT0rrB&coPiYoZ<>eLBKGXP#esf0sx8-w6 zKEJH3(UWgnlBkQ*(bTy-W#2A4!os5W9sdOFe!;DL!h_VD#oZ!Bdex>ZO{0}{f BW_