Avoid copies of string preprocess objects

Only one instance of this class should exist for a program.

Author: romainbrenguier

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -31,7 +31,7 @@ class java_bytecode_convert_classt:public messaget
     size_t _max_array_length,
     lazy_methodst& _lazy_methods,
     lazy_methods_modet _lazy_methods_mode,
-    const java_string_library_preprocesst &_string_preprocess):
+    java_string_library_preprocesst &_string_preprocess):
     messaget(_message_handler),
     symbol_table(_symbol_table),
     max_array_length(_max_array_length),
@@ -63,7 +63,7 @@ class java_bytecode_convert_classt:public messaget
   const size_t max_array_length;
   lazy_methodst &lazy_methods;
   lazy_methods_modet lazy_methods_mode;
-  java_string_library_preprocesst string_preprocess;
+  java_string_library_preprocesst &string_preprocess;
 
   // conversion
   void convert(const classt &c);
@@ -477,7 +477,7 @@ bool java_bytecode_convert_class(
   size_t max_array_length,
   lazy_methodst &lazy_methods,
   lazy_methods_modet lazy_methods_mode,
-  const java_string_library_preprocesst &string_preprocess)
+  java_string_library_preprocesst &string_preprocess)
 {
   java_bytecode_convert_classt java_bytecode_convert_class(
     symbol_table,

src/java_bytecode/java_bytecode_convert_class.h

@@ -22,6 +22,6 @@ bool java_bytecode_convert_class(
   size_t max_array_length,
   lazy_methodst &,
   lazy_methods_modet,
-  const java_string_library_preprocesst &string_preprocess);
+  java_string_library_preprocesst &string_preprocess);
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -2777,7 +2777,7 @@ void java_bytecode_convert_method(
   message_handlert &message_handler,
   size_t max_array_length,
   safe_pointer<ci_lazy_methodst> lazy_methods,
-  const java_string_library_preprocesst &string_preprocess)
+  java_string_library_preprocesst &string_preprocess)
 {
   static const std::unordered_set<std::string> methods_to_ignore
   {

src/java_bytecode/java_bytecode_convert_method.h

@@ -26,15 +26,15 @@ void java_bytecode_convert_method(
   message_handlert &message_handler,
   size_t max_array_length,
   safe_pointer<ci_lazy_methodst> lazy_methods,
-  const java_string_library_preprocesst &string_preprocess);
+  java_string_library_preprocesst &string_preprocess);
 
 inline void java_bytecode_convert_method(
   const symbolt &class_symbol,
   const java_bytecode_parse_treet::methodt &method,
   symbol_tablet &symbol_table,
   message_handlert &message_handler,
   size_t max_array_length,
-  const java_string_library_preprocesst &string_preprocess)
+  java_string_library_preprocesst &string_preprocess)
 {
   java_bytecode_convert_method(
     class_symbol,

src/java_bytecode/java_bytecode_convert_method_class.h

@@ -33,7 +33,7 @@ class java_bytecode_convert_methodt:public messaget
     message_handlert &_message_handler,
     size_t _max_array_length,
     safe_pointer<ci_lazy_methodst> _lazy_methods,
-    const java_string_library_preprocesst &_string_preprocess):
+    java_string_library_preprocesst &_string_preprocess):
     messaget(_message_handler),
     symbol_table(_symbol_table),
     max_array_length(_max_array_length),
@@ -61,7 +61,7 @@ class java_bytecode_convert_methodt:public messaget
   irep_idt method_id;
   irep_idt current_method;
   typet method_return_type;
-  java_string_library_preprocesst string_preprocess;
+  java_string_library_preprocesst &string_preprocess;
 
 public:
   struct holet

src/java_bytecode/java_string_library_preprocess.h

@@ -47,6 +47,9 @@ class java_string_library_preprocesst:public messaget
   bool is_known_string_type(irep_idt class_name);
 
 private:
+  // We forbid copies of the object by making the copy operator private.
+  java_string_library_preprocesst(const java_string_library_preprocesst &);
+
   static bool java_type_matches_tag(const typet &type, const std::string &tag);
   static bool is_java_string_pointer_type(const typet &type);
   static bool is_java_string_type(const typet &type);