add java_utils.cpp

Author: mgudemann

src/java_bytecode/java_object_factory.cpp

@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_object_factory.h"
 #include "java_types.h"
+#include "java_utils.h"
 
 /*******************************************************************\
 
@@ -223,11 +224,8 @@ void java_object_factoryt::gen_nondet_init(
       init_code.move_to_operands(null_check);
     }
 
-    if(subtype.id()==ID_struct &&
-       has_prefix(id2string(to_struct_type(subtype).get_tag()), "java::array["))
-    {
+    if(java_is_array_type(subtype))
       gen_nondet_array_init(expr, loc);
-    }
     else
     {
       exprt allocated=

src/java_bytecode/java_utils.cpp

@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include <util/prefix.h>
+#include <util/std_types.h>
+
+#include "java_utils.h"
+
+bool java_is_array_type(const typet &type)
+{
+  if(type.id()!=ID_struct)
+    return false;
+  return has_prefix(id2string(
+    to_struct_type(type).get_tag()),
+                    "java::array[");
+}

src/java_bytecode/java_utils.h

@@ -0,0 +1,16 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include <util/type.h>
+
+#ifndef CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
+#define CPROVER_JAVA_BYTECODE_JAVA_UTILS_H
+
+bool java_is_array_type(const typet &type);
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H