Changes to get java compiling

Author: thk123

src/java_bytecode/java_entry_point.h

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/irep.h>
 
+#define JAVA_ENTRY_POINT_RETURN_SYMBOL "return'"
+
 bool java_entry_point(
   class symbol_tablet &symbol_table,
   const irep_idt &main_class,

src/java_bytecode/java_object_factory.cpp

@@ -483,7 +483,8 @@ void gen_nondet_init(
   bool create_dyn_objs,
   bool assume_non_null,
   message_handlert &message_handler,
-  size_t max_nondet_array_length)
+  size_t max_nondet_array_length,
+  update_in_placet update_in_place)
 {
   java_object_factoryt state(
     init_code,

src/java_bytecode/java_object_factory.h

@@ -22,6 +22,13 @@ exprt object_factory(
   const source_locationt &,
   message_handlert &message_handler);
 
+enum update_in_placet
+{
+  NO_UPDATE_IN_PLACE,
+  MAY_UPDATE_IN_PLACE,
+  MUST_UPDATE_IN_PLACE
+};
+
 void gen_nondet_init(
   const exprt &expr,
   code_blockt &init_code,
@@ -31,7 +38,8 @@ void gen_nondet_init(
   bool create_dynamic_objects,
   bool assume_non_null,
   message_handlert &message_handler,
-  size_t max_nondet_array_length=5);
+  size_t max_nondet_array_length,
+  update_in_placet update_in_place=NO_UPDATE_IN_PLACE);
 
 
 exprt get_nondet_bool(const typet &);

src/java_bytecode/java_types.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 #include <cctype>
 
+#include <util/prefix.h>
 #include <util/std_types.h>
 #include <util/std_expr.h>
 #include <util/ieee_float.h>
@@ -231,6 +232,23 @@ pointer_typet java_array_type(const char subtype)
 
 /*******************************************************************\
 
+Function: is_java_array_tag
+
+  Inputs: Struct tag 'tag'
+
+ Outputs: True if the given struct is a Java array
+
+ Purpose: See above
+
+\*******************************************************************/
+
+bool is_java_array_tag(const irep_idt& tag)
+{
+  return has_prefix(id2string(tag), "java::array[");
+}
+
+/*******************************************************************\
+
 Function: is_reference_type
 
   Inputs:

src/java_bytecode/java_types.h

@@ -44,4 +44,6 @@ char java_char_from_type(const typet &type);
 typet java_bytecode_promotion(const typet &);
 exprt java_bytecode_promotion(const exprt &);
 
+bool is_java_array_tag(const irep_idt& tag);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H