@@ -785,18 +785,29 @@ void java_object_factoryt::gen_nondet_pointer_init(
785
785
// (This can currently happen for some cases of #exception_value)
786
786
bool must_be_null = subtype == empty_typet ();
787
787
788
- // If we may be about to initialize a non-null object , always run the
788
+ // If we may be about to initialize a non-null enum type , always run the
789
789
// clinit_wrapper of its class first.
790
+ // TODO: TG-4689 we may want to do this for all types, not just enums, as
791
+ // described in the Java language specification:
792
+ // https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.7
793
+ // https://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4.1
794
+ // But we would have to put this behavior behind an option as it would have an
795
+ // impact on running times.
790
796
// Note that it would be more consistent with the behaviour of the JVM to only
791
797
// run clinit_wrapper if we are about to initialize an object of which we know
792
798
// for sure that it is not null on any following branch. However, adding this
793
- // case in gen_nondet_struct_init would slow symex down too much.
794
- if (!must_be_null)
799
+ // case in gen_nondet_struct_init would slow symex down too much, so if we
800
+ // decide to do this for all types, we should do it here.
801
+ // Note also that this logic is mirrored in
802
+ // ci_lazy_methodst::initialize_instantiated_classes.
803
+ if (const auto class_type = type_try_dynamic_cast<java_class_typet>(subtype))
795
804
{
796
- const java_class_typet &class_type = to_java_class_type (subtype);
797
- const irep_idt &class_name = class_type.get_name ();
798
- const irep_idt class_clinit = clinit_wrapper_name (class_name);
799
- gen_method_call_if_present (assignments, expr, class_clinit);
805
+ if (class_type->get_base (" java::java.lang.Enum" ) && !must_be_null)
806
+ {
807
+ const irep_idt &class_name = class_type->get_name ();
808
+ const irep_idt class_clinit = clinit_wrapper_name (class_name);
809
+ gen_method_call_if_present (assignments, expr, class_clinit);
810
+ }
800
811
}
801
812
802
813
code_blockt new_object_assignments;
0 commit comments