diff --git a/jbmc/src/java_bytecode/expr2java.h b/jbmc/src/java_bytecode/expr2java.h index cfb4d5a8286..4d04699b109 100644 --- a/jbmc/src/java_bytecode/expr2java.h +++ b/jbmc/src/java_bytecode/expr2java.h @@ -58,8 +58,8 @@ std::string type2java(const typet &type, const namespacet &ns); template std::string floating_point_to_java_string(float_type value) { - static const bool is_float = std::is_same::value; - static const std::string class_name = is_float ? "Float" : "Double"; + const bool is_float = std::is_same::value; + const std::string class_name = is_float ? "Float" : "Double"; if(std::isnan(value)) return class_name + ".NaN"; if(std::isinf(value) && value >= 0.) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 5c15f43abee..8156d102237 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -845,7 +845,7 @@ const select_pointer_typet & void java_bytecode_languaget::methods_provided( std::unordered_set &methods) const { - static std::string cprover_class_prefix = "java::org.cprover.CProver."; + const std::string cprover_class_prefix = "java::org.cprover.CProver."; // Add all string solver methods to map string_preprocess.get_all_function_names(methods); diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp index 9553e3a4544..bb61c887288 100644 --- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp @@ -301,9 +301,9 @@ class base_ref_infot : public structured_pool_entryt public: explicit base_ref_infot(pool_entryt entry) : structured_pool_entryt(entry) { - static std::set info_tags = { - CONSTANT_Fieldref, CONSTANT_Methodref, CONSTANT_InterfaceMethodref}; - PRECONDITION(info_tags.find(entry.tag) != info_tags.end()); + PRECONDITION( + entry.tag == CONSTANT_Fieldref || entry.tag == CONSTANT_Methodref || + entry.tag == CONSTANT_InterfaceMethodref); class_index = entry.ref1; name_and_type_index = entry.ref2; } diff --git a/jbmc/src/java_bytecode/load_method_by_regex.cpp b/jbmc/src/java_bytecode/load_method_by_regex.cpp index 22468317495..e5ce7eb0d5f 100644 --- a/jbmc/src/java_bytecode/load_method_by_regex.cpp +++ b/jbmc/src/java_bytecode/load_method_by_regex.cpp @@ -41,7 +41,7 @@ bool does_pattern_miss_descriptor(const std::string &pattern) if(descriptor_index == std::string::npos) return true; - static const std::string java_prefix = "java::"; + const std::string java_prefix = "java::"; return descriptor_index == java_prefix.length() - 1 && has_prefix(pattern, java_prefix); }