Skip to content

Commit 7191f23

Browse files
committed
Do not unnecessarily mark local variables static
1 parent 9480092 commit 7191f23

File tree

4 files changed

+7
-7
lines changed

4 files changed

+7
-7
lines changed

jbmc/src/java_bytecode/expr2java.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -58,8 +58,8 @@ std::string type2java(const typet &type, const namespacet &ns);
5858
template <typename float_type>
5959
std::string floating_point_to_java_string(float_type value)
6060
{
61-
static const bool is_float = std::is_same<float_type, float>::value;
62-
static const std::string class_name = is_float ? "Float" : "Double";
61+
const bool is_float = std::is_same<float_type, float>::value;
62+
const std::string class_name = is_float ? "Float" : "Double";
6363
if(std::isnan(value))
6464
return class_name + ".NaN";
6565
if(std::isinf(value) && value >= 0.)

jbmc/src/java_bytecode/java_bytecode_language.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -845,7 +845,7 @@ const select_pointer_typet &
845845
void java_bytecode_languaget::methods_provided(
846846
std::unordered_set<irep_idt> &methods) const
847847
{
848-
static std::string cprover_class_prefix = "java::org.cprover.CProver.";
848+
const std::string cprover_class_prefix = "java::org.cprover.CProver.";
849849

850850
// Add all string solver methods to map
851851
string_preprocess.get_all_function_names(methods);

jbmc/src/java_bytecode/java_bytecode_parser.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -301,9 +301,9 @@ class base_ref_infot : public structured_pool_entryt
301301
public:
302302
explicit base_ref_infot(pool_entryt entry) : structured_pool_entryt(entry)
303303
{
304-
static std::set<u1> info_tags = {
305-
CONSTANT_Fieldref, CONSTANT_Methodref, CONSTANT_InterfaceMethodref};
306-
PRECONDITION(info_tags.find(entry.tag) != info_tags.end());
304+
PRECONDITION(
305+
entry.tag == CONSTANT_Fieldref || entry.tag == CONSTANT_Methodref ||
306+
entry.tag == CONSTANT_InterfaceMethodref);
307307
class_index = entry.ref1;
308308
name_and_type_index = entry.ref2;
309309
}

jbmc/src/java_bytecode/load_method_by_regex.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ bool does_pattern_miss_descriptor(const std::string &pattern)
4141
if(descriptor_index == std::string::npos)
4242
return true;
4343

44-
static const std::string java_prefix = "java::";
44+
const std::string java_prefix = "java::";
4545
return descriptor_index == java_prefix.length() - 1 &&
4646
has_prefix(pattern, java_prefix);
4747
}

0 commit comments

Comments
 (0)