Improve documentation for java array types

Author: svorenova

jbmc/src/java_bytecode/java_types.cpp

@@ -87,6 +87,10 @@ reference_typet java_lang_object_type()
   return java_reference_type(symbol_typet("java::java.lang.Object"));
 }
 
+/// Construct an array pointer type. It is a pointer to a symbol with identifier
+/// java::array[]. Its ID_C_element_type is set to the corresponding primitive
+/// type, or void* for arrays of references.
+/// \param subtype Character indicating the type of array
 reference_typet java_array_type(const char subtype)
 {
   std::string subtype_str;
@@ -160,13 +164,24 @@ bool is_multidim_java_array_type(const typet &type)
 }
 
 /// See above
-/// \par parameters: Struct tag 'tag'
-/// \return True if the given struct is a Java array
+/// \param tag Tag of a struct
+/// \return True if the given string is a Java array tag, i.e., has a prefix
+/// of java::array[
 bool is_java_array_tag(const irep_idt& tag)
 {
   return has_prefix(id2string(tag), "java::array[");
 }
 
+/// Constructs a type indicated by the given character:
+/// - i  integer
+/// - l  long
+/// - s  short
+/// - b  byte
+/// - c  character
+/// - f  float
+/// - d  double
+/// - z  boolean
+/// - a  reference
 typet java_type_from_char(char t)
 {
   switch(t)

jbmc/src/java_bytecode/java_types.h

@@ -250,16 +250,6 @@ typet &java_array_element_type(symbol_typet &array_symbol);
 bool is_java_array_type(const typet &type);
 bool is_multidim_java_array_type(const typet &type);
 
-// i  integer
-// l  long
-// s  short
-// b  byte
-// c  character
-// f  float
-// d  double
-// z  boolean
-// a  reference
-
 typet java_type_from_char(char t);
 typet java_type_from_string(
   const std::string &,