Merge pull request #4767 from jeannielynnmoulton/jeannie/UserSpecifiedClinitCheck

Function and test for identifier of user specified clinit [TG-7981]

Author: jeannielynnmoulton

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -88,6 +88,14 @@ bool is_clinit_function(const irep_idt &function_id)
   return has_suffix(id2string(function_id), clinit_function_suffix);
 }
 
+/// Check if function_id is a user-specified clinit
+/// \param function_id: some function identifier
+/// \return true if the passed identifier is a clinit
+bool is_user_specified_clinit_function(const irep_idt &function_id)
+{
+  return has_suffix(id2string(function_id), user_specified_clinit_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

@@ -26,6 +26,7 @@ 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);
+bool is_user_specified_clinit_function(const irep_idt &function_id);
 
 void create_static_initializer_symbols(
   symbol_tablet &symbol_table,

jbmc/unit/java_bytecode/java_static_initializers/java_static_initializers.cpp

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
-Module: Unit tests for java_types
+Module: Unit tests for java_static_initializers
 
 Author: Diffblue Ltd.
 
@@ -12,15 +12,43 @@ Author: Diffblue Ltd.
 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));
+    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));
+    THEN("is_clinit_function should return false.")
+    {
+      const std::string input =
+        "com.something.package.TestClass.<notclinit>:()V";
+      REQUIRE_FALSE(is_clinit_function(input));
+    }
+  }
+}
+
+SCENARIO(
+  "is_user_specified_clinit_function",
+  "[core][java_static_initializers]")
+{
+  GIVEN("A function id that represents a user-specified clinit")
+  {
+    THEN("is_user_specified_clinit_function should return true.")
+    {
+      const std::string input =
+        "com.something.package.TestClass::user_specified_clinit";
+      REQUIRE(is_user_specified_clinit_function(input));
+    }
+  }
+  GIVEN("A function id that does not represent a user-specified clinit")
+  {
+    THEN("is_clinit_function should return false.")
+    {
+      const std::string input = "com.something.package.TestClass::not_it";
+      REQUIRE_FALSE(is_user_specified_clinit_function(input));
+    }
   }
 }