Unit test to demonstrate issue in make_object_get_class_code

Author: Nathan Phillips

unit/java_bytecode/java_string_library_preprocess/Class.class

@@ -0,0 +1,13 @@
+package java.lang;
+
+class Class {
+    static Class forName(String className) {
+        return null;
+    }
+}
+
+public class TestObjectGetClass {
+    void main() {
+        this.getClass();
+    }
+}

unit/java_bytecode/java_string_library_preprocess/TestObjectGetClass.class

@@ -0,0 +1,36 @@
+/// file
+/// Test for types in return value of make_object_get_class_code
+
+/// Author: Diffblue Ltd.
+
+#include <testing-utils/catch.hpp>
+#include <util/symbol_table.h>
+#include <testing-utils/load_java_class.h>
+
+TEST_CASE("Check types of return value of make_object_get_class_code")
+{
+  GIVEN("")
+  {
+    symbol_tablet symbol_table = load_java_class("TestObjectGetClass", ".", true);
+    for(auto &named_symbol : symbol_table.symbols)
+    {
+      named_symbol.first;
+    }
+
+    code_typet::parametert param;
+    param.set_identifier("this");
+    code_typet type;
+    type.parameters().push_back(param);
+    source_locationt loc;
+    loc.
+    symbol_tablet symbol_table;
+    WHEN("")
+    {
+      THEN("The type of the returned expression is that of refined strings")
+      {
+        code_for_function("java::java.lang.Object.getClass:()Ljava/lang/Class;", type, loc, symbol_table);
+        REQUIRE(string_expr.id() == ID_struct);
+      }
+    }
+  }
+}

unit/java_bytecode/java_string_library_preprocess/TestObjectGetClass.java

@@ -25,7 +25,8 @@
 /// \return The symbol table that is generated by parsing this file.
 symbol_tablet load_java_class(
   const std::string &java_class_name,
-  const std::string &class_path)
+  const std::string &class_path,
+  bool use_string_refinement)
 {
   return load_java_class(
     java_class_name, class_path, new_java_bytecode_language());
@@ -34,6 +35,7 @@ symbol_tablet load_java_class(
 symbol_tablet load_java_class(
   const std::string &java_class_name,
   const std::string &class_path,
+  bool use_string_refinement,
   std::unique_ptr<languaget> java_lang)
 {
   // We don't expect the .class suffix to allow us to check the name of the
@@ -43,6 +45,8 @@ symbol_tablet load_java_class(
   // Configure the path loading
   cmdlinet command_line;
   command_line.set("java-cp-include-files", class_path);
+  if(use_string_refinement)
+    command_line.set("refine-strings", true);
   config.java.classpath.clear();
   config.java.classpath.push_back(class_path);
 

unit/java_bytecode/java_string_library_preprocess/make_object_get_class_code.cpp

@@ -19,11 +19,13 @@
 
 symbol_tablet load_java_class(
   const std::string &java_class_name,
-  const std::string &class_path);
+  const std::string &class_path,
+  bool use_string_refinement = false);
 
 symbol_tablet load_java_class(
   const std::string &java_class_name,
   const std::string &class_path,
+  bool use_string_refinement,
   std::unique_ptr<languaget> java_lang);
 
 #endif // CPROVER_TESTING_UTILS_LOAD_JAVA_CLASS_H