Merge pull request #4706 from jeannielynnmoulton/jeannie/ClinitCheck

Add function that checks if function id represents a clinit.

Author: jeannielynnmoulton

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -80,6 +80,14 @@ bool is_clinit_wrapper_function(const irep_idt &function_id)
   return has_suffix(id2string(function_id), clinit_wrapper_suffix);
 }
 
+/// Check if function_id is a clinit
+/// \param function_id: some function identifier
+/// \return true if the passed identifier is a clinit
+bool is_clinit_function(const irep_idt &function_id)
+{
+  return has_suffix(id2string(function_id), clinit_function_suffix);
+}
+
 /// Add a new symbol to the symbol table.
 /// Note: assumes that a symbol with this name does not exist.
 /// /param name: name of the symbol to be generated

jbmc/src/java_bytecode/java_static_initializers.h

@@ -25,6 +25,7 @@ irep_idt clinit_wrapper_name(const irep_idt &class_name);
 irep_idt user_specified_clinit_name(const irep_idt &class_name);
 
 bool is_clinit_wrapper_function(const irep_idt &function_id);
+bool is_clinit_function(const irep_idt &function_id);
 
 void create_static_initializer_symbols(
   symbol_tablet &symbol_table,

jbmc/unit/Makefile

@@ -47,6 +47,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \
        java_bytecode/java_object_factory/gen_nondet_string_init.cpp \
        java_bytecode/java_object_factory/struct_tag_types.cpp \
        java_bytecode/java_replace_nondet/replace_nondet.cpp \
+       java_bytecode/java_static_initializers/java_static_initializers.cpp \
        java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \
        java_bytecode/java_types/erase_type_arguments.cpp \
        java_bytecode/java_types/generic_type_index.cpp \

jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp

@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+Module: Unit tests for java_types
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#include <java_bytecode/java_static_initializers.h>
+#include <testing-utils/use_catch.h>
+
+SCENARIO("is_clinit_function", "[core][java_static_initializers]")
+{
+  GIVEN("A function id that represents a clinit")
+  THEN("is_clinit_function should return true.")
+  {
+    const std::string input = "com.something.package.TestClass.<clinit>:()V";
+    REQUIRE(is_clinit_function(input));
+  }
+  GIVEN("A function id that does not represent a clinit")
+  THEN("is_clinit_function should return false.")
+  {
+    const std::string input = "com.something.package.TestClass.<notclinit>:()V";
+    REQUIRE_FALSE(is_clinit_function(input));
+  }
+}

jbmc/unit/java_bytecode/java_static_initializers/module_dependencies.txt

@@ -0,0 +1,2 @@
+java_bytecode
+testing-utils