Add identifier and rename statement to java_new_array_data

This will be used as an alternative to java_new_array.
This is to distinguish the statement before and after symex:
java_new_array is used before symex, it is then transformed into some
instrtuction containing a java_new_array_data by symex.
Symex use to add a new java_new_array statement which was confusing.

Author: romainbrenguier

src/goto-programs/builtin_functions.cpp

@@ -705,7 +705,8 @@ void goto_convertt::do_java_new_array(
   else
     allocate_data_type=data.type();
 
-  side_effect_exprt data_java_new_expr(ID_java_new_array, allocate_data_type);
+  side_effect_exprt data_java_new_expr(
+    ID_java_new_array_data, allocate_data_type);
 
   // The instruction may specify a (hopefully small) upper bound on the
   // array size, in which case we allocate a fixed-length array that may

src/goto-programs/goto_convert.cpp

@@ -760,8 +760,10 @@ void goto_convertt::convert_assign(
 
     do_java_new_array(lhs, to_side_effect_expr(rhs), dest);
   }
-  else if(rhs.id()==ID_side_effect &&
-          rhs.get(ID_statement)==ID_malloc)
+  else if(
+    rhs.id() == ID_side_effect &&
+    (rhs.get(ID_statement) == ID_malloc ||
+     rhs.get(ID_statement) == ID_java_new_array_data))
   {
     // just preserve
     Forall_operands(it, rhs)

src/goto-symex/symex_assign.cpp

@@ -59,9 +59,9 @@ void goto_symext::symex_assign(
 
       throw "symex_assign: unexpected function call: "+id2string(identifier);
     }
-    else if(statement==ID_cpp_new ||
-            statement==ID_cpp_new_array ||
-            statement==ID_java_new_array)
+    else if(
+      statement == ID_cpp_new || statement == ID_cpp_new_array ||
+      statement == ID_java_new_array_data)
       symex_cpp_new(state, lhs, side_effect_expr);
     else if(statement==ID_malloc)
       symex_malloc(state, lhs, side_effect_expr);

src/goto-symex/symex_builtin_functions.cpp

@@ -376,8 +376,9 @@ void goto_symext::symex_cpp_new(
   if(code.type().id()!=ID_pointer)
     throw "new expected to return pointer";
 
-  do_array=(code.get(ID_statement)==ID_cpp_new_array ||
-            code.get(ID_statement)==ID_java_new_array);
+  do_array =
+    (code.get(ID_statement) == ID_cpp_new_array ||
+     code.get(ID_statement) == ID_java_new_array_data);
 
   dynamic_counter++;
 
@@ -393,7 +394,7 @@ void goto_symext::symex_cpp_new(
   if(code.get(ID_statement)==ID_cpp_new_array ||
      code.get(ID_statement)==ID_cpp_new)
     symbol.mode=ID_cpp;
-  else if(code.get(ID_statement)==ID_java_new_array)
+  else if(code.get(ID_statement) == ID_java_new_array_data)
     symbol.mode=ID_java;
   else
     INVARIANT_WITH_IREP(false, "Unexpected side effect expression", code);

src/util/irep_ids.def

@@ -217,6 +217,7 @@ IREP_ID_TWO(cpp_new_array, cpp_new[])
 IREP_ID_TWO(cpp_delete_array, cpp_delete[])
 IREP_ID_ONE(java_new)
 IREP_ID_ONE(java_new_array)
+IREP_ID_ONE(java_new_array_data)
 IREP_ID_ONE(java_string_literal)
 IREP_ID_ONE(printf)
 IREP_ID_ONE(input)