Added overload with the identiy pointer_selector

Author: thk123

src/goto-programs/convert_nondet.cpp

@@ -89,7 +89,6 @@ static goto_programt::targett insert_nondet_init_code(
     allocation_typet::DYNAMIC,
     !nullable,
     max_nondet_array_length,
-    std::make_shared<select_pointer_typet>(),
     update_in_placet::NO_UPDATE_IN_PLACE);
 
   // Convert this code into goto instructions

src/java_bytecode/java_bytecode_instrument.cpp

@@ -114,8 +114,7 @@ codet java_bytecode_instrumentt::throw_exception(
       symbol_table,
       max_array_length,
       allocation_typet::LOCAL,
-      original_loc,
-      std::make_shared<select_pointer_typet>());
+      original_loc);
   }
   else
     exc=symbol_table.lookup(exc_obj_name).symbol_expr();

src/java_bytecode/java_object_factory.cpp

@@ -1071,3 +1071,49 @@ void gen_nondet_init(
 
   init_code.append(assignments);
 }
+
+/// Call object_factory with a default (identity) pointer_type_selector
+exprt object_factory(const typet &type,
+  const irep_idt base_name,
+  code_blockt &init_code,
+  bool allow_null,
+  symbol_tablet &symbol_table,
+  size_t max_nondet_array_length,
+  allocation_typet alloc_type,
+  const source_locationt &location)
+{
+  return object_factory(
+    type,
+    base_name,
+    init_code,
+    allow_null,
+    symbol_table,
+    max_nondet_array_length,
+    alloc_type,
+    location,
+    std::make_shared<select_pointer_typet>());
+}
+
+/// Call gen_nondet_init with a default (identity) pointer_type_selector
+void gen_nondet_init(const exprt &expr,
+  code_blockt &init_code,
+  symbol_tablet &symbol_table,
+  const source_locationt &loc,
+  bool skip_classid,
+  allocation_typet alloc_type,
+  bool assume_non_null,
+  size_t max_nondet_array_length,
+  update_in_placet update_in_place)
+{
+  gen_nondet_init(
+    expr,
+    init_code,
+    symbol_table,
+    loc,
+    skip_classid,
+    alloc_type,
+    assume_non_null,
+    max_nondet_array_length,
+    std::make_shared<select_pointer_typet>(),
+    update_in_place);
+}

src/java_bytecode/java_object_factory.h

@@ -38,6 +38,16 @@ exprt object_factory(
   const source_locationt &location,
   std::shared_ptr<select_pointer_typet> pointer_type_selector);
 
+exprt object_factory(
+  const typet &type,
+  const irep_idt base_name,
+  code_blockt &init_code,
+  bool allow_null,
+  symbol_tablet &symbol_table,
+  size_t max_nondet_array_length,
+  allocation_typet alloc_type,
+  const source_locationt &location);
+
 enum class update_in_placet
 {
   NO_UPDATE_IN_PLACE,
@@ -57,6 +67,17 @@ void gen_nondet_init(
   std::shared_ptr<select_pointer_typet> pointer_type_selector,
   update_in_placet update_in_place);
 
+void gen_nondet_init(
+  const exprt &expr,
+  code_blockt &init_code,
+  symbol_tablet &symbol_table,
+  const source_locationt &loc,
+  bool skip_classid,
+  allocation_typet alloc_type,
+  bool assume_non_null,
+  size_t max_nondet_array_length,
+  update_in_placet update_in_place);
+
 exprt allocate_dynamic_object(
   const exprt &target_expr,
   const typet &allocate_type,