From 5a349f0ff4def7a742401b3653697172b5f71fda Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 6 Dec 2016 16:53:53 +0000 Subject: [PATCH] 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. --- src/java_bytecode/java_bytecode_typecheck.cpp | 6 ++++++ src/java_bytecode/java_bytecode_typecheck.h | 4 ++-- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_bytecode_typecheck.cpp b/src/java_bytecode/java_bytecode_typecheck.cpp index e72b80a885d..9e1c5f2a732 100644 --- a/src/java_bytecode/java_bytecode_typecheck.cpp +++ b/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 + java_bytecode_typecheckt::string_literal_to_symbol_name; +std::map + java_bytecode_typecheckt::escaped_string_literal_count; diff --git a/src/java_bytecode/java_bytecode_typecheck.h b/src/java_bytecode/java_bytecode_typecheck.h index e22a9db545b..7b12a4ffbb5 100644 --- a/src/java_bytecode/java_bytecode_typecheck.h +++ b/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 already_typechecked; - std::map string_literal_to_symbol_name; - std::map escaped_string_literal_count; + static std::map string_literal_to_symbol_name; + static std::map escaped_string_literal_count; }; #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_TYPECHECK_H