diff --git a/regression/cbmc-java/lazyloading5/other.class b/regression/cbmc-java/lazyloading5/other.class new file mode 100644 index 00000000000..88dbb5d67c2 Binary files /dev/null and b/regression/cbmc-java/lazyloading5/other.class differ diff --git a/regression/cbmc-java/lazyloading5/test.class b/regression/cbmc-java/lazyloading5/test.class new file mode 100644 index 00000000000..b2f426a182a Binary files /dev/null and b/regression/cbmc-java/lazyloading5/test.class differ diff --git a/regression/cbmc-java/lazyloading5/test.desc b/regression/cbmc-java/lazyloading5/test.desc new file mode 100644 index 00000000000..a3226adccaa --- /dev/null +++ b/regression/cbmc-java/lazyloading5/test.desc @@ -0,0 +1,6 @@ +CORE +test.class +--lazy-methods --function test.main +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL diff --git a/regression/cbmc-java/lazyloading5/test.java b/regression/cbmc-java/lazyloading5/test.java new file mode 100644 index 00000000000..351f844655b --- /dev/null +++ b/regression/cbmc-java/lazyloading5/test.java @@ -0,0 +1,21 @@ + +public class test { + + public static void main() { + + assert(other.getx()==1); + + } + +} + +class other { + + public static int x; + public static int getx() { return x; } + + static { + x=1; + } + +} diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index ad70b5cd041..6137931617f 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1418,7 +1418,11 @@ codet java_bytecode_convert_methodt::convert_instructions( // static binding call.function()=symbol_exprt(arg0.get(ID_identifier), arg0.type()); if(lazy_methods) + { lazy_methods->add_needed_method(arg0.get(ID_identifier)); + // Calling a static method causes static initialization: + lazy_methods->add_needed_class(arg0.get(ID_C_class)); + } } call.function().add_source_location()=loc;