Make string literal tables global

The string literal uniqueing tables only work if they can see every string in the program, and if multiple .class files are specified on the command-line, multiple java_bytecode_typecheckt instances are created. Literal symbol creation would then fail if the two classes used matching literals. Note this does not apply to classes loaded on demand or from a JAR file, which *do* share a typecheckt instance with their parent.

Author: smowton

src/java_bytecode/java_bytecode_typecheck.cpp

@@ -184,3 +184,9 @@ bool java_bytecode_typecheck(
   // fail for now
   return true;
 }
+
+// Static members of java_bytecode_typecheckt:
+std::map<irep_idt, irep_idt>
+  java_bytecode_typecheckt::string_literal_to_symbol_name;
+std::map<irep_idt, size_t>
+  java_bytecode_typecheckt::escaped_string_literal_count;

src/java_bytecode/java_bytecode_typecheck.h

@@ -64,8 +64,8 @@ class java_bytecode_typecheckt:public typecheckt
   virtual std::string to_string(const typet &type);
 
   std::set<irep_idt> already_typechecked;
-  std::map<irep_idt, irep_idt> string_literal_to_symbol_name;
-  std::map<irep_idt, size_t> escaped_string_literal_count;
+  static std::map<irep_idt, irep_idt> string_literal_to_symbol_name;
+  static std::map<irep_idt, size_t> escaped_string_literal_count;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H