Use is_valid_java_array function

antlechner · antlechner · commit cef34e0d2a42 · 2018-08-10T18:43:10.000+01:00
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -400,7 +400,7 @@ void java_object_factoryt::gen_pointer_target_init(
   if(target_type.id() == ID_struct)
   {
     const auto &target_class_type = to_java_class_type(target_type);
-    if(has_prefix(id2string(target_class_type.get_tag()), "java::array["))
+    if(is_valid_java_array(target_class_type))
     {
       gen_nondet_array_init(
         assignments, expr, depth + 1, update_in_place, location);

Original file line number	Diff line number	Diff line change
`@@ -400,7 +400,7 @@ void java_object_factoryt::gen_pointer_target_init(`
`400`	`400`	`if(target_type.id() == ID_struct)`
`401`	`401`	`{`
`402`	`402`	`const auto &target_class_type = to_java_class_type(target_type);`
`403`		`- if(has_prefix(id2string(target_class_type.get_tag()), "java::array["))`
	`403`	`+ if(is_valid_java_array(target_class_type))`
`404`	`404`	`{`
`405`	`405`	`gen_nondet_array_init(`
`406`	`406`	`assignments, expr, depth + 1, update_in_place, location);`