Added invariants on the correct structure of the array type

Added to converting types and when creating non det initilization.

Author: thk123

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -292,6 +292,11 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     comp2.set_base_name("data");
     struct_type.components().push_back(comp2);
 
+    INVARIANT(
+      is_valid_java_array(struct_type),
+      "Constructed a new type representing a Java Array "
+      "object that doesn't match expectations");
+
     symbolt symbol;
     symbol.name=symbol_type.get_identifier();
     symbol.base_name=symbol_type.get(ID_C_base_name);

src/java_bytecode/java_object_factory.cpp

@@ -1059,6 +1059,10 @@ void java_object_factoryt::gen_nondet_array_init(
   // Otherwise we're updating the array in place, and use the
   // existing array allocation and length.
 
+  INVARIANT(
+    is_valid_java_array(struct_type),
+    "Java struct array does not conform to expectations");
+
   dereference_exprt deref_expr(expr, expr.type().subtype());
   const auto &comps=struct_type.components();
   exprt length_expr=member_exprt(deref_expr, "length", comps[1].type());