Merge pull request #4455 from thomasspriggs/tas/id_c_class

Standardise interface for accessing the owner of a symbol

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -689,10 +689,9 @@ void java_bytecode_convert_classt::convert(
     new_symbol.name=id2string(class_symbol.name)+"."+id2string(f.name);
     new_symbol.base_name=f.name;
     new_symbol.type=field_type;
-    // Annotating the type with ID_C_class to provide a static field -> class
-    // link matches the method used by java_bytecode_convert_method::convert
-    // for methods.
-    new_symbol.type.set(ID_C_class, class_symbol.name);
+    // Provide a static field -> class link, like
+    // java_bytecode_convert_method::convert does for method -> class.
+    set_declaring_class(new_symbol, class_symbol.name);
     new_symbol.type.set(ID_C_field, f.name);
     new_symbol.type.set(ID_C_constant, f.is_final);
     new_symbol.pretty_name=id2string(class_symbol.pretty_name)+

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -419,6 +419,8 @@ void java_bytecode_convert_methodt::convert(
     get_method_identifier(class_symbol.name, m);
 
   method_id=method_identifier;
+  set_declaring_class(
+    symbol_table.get_writeable_ref(method_identifier), class_symbol.name);
 
   // Obtain a std::vector of java_method_typet::parametert objects from the
   // (function) type of the symbol
@@ -428,7 +430,6 @@ void java_bytecode_convert_methodt::convert(
   // to the symbol later.
   java_method_typet method_type =
     to_java_method_type(symbol_table.lookup_ref(method_identifier).type);
-  method_type.set(ID_C_class, class_symbol.name);
   method_type.set_is_final(m.is_final);
   method_return_type = method_type.return_type();
   java_method_typet::parameterst &parameters = method_type.parameters();
@@ -2206,6 +2207,7 @@ void java_bytecode_convert_methodt::convert_invoke(
     symbol.mode = ID_java;
     assign_parameter_names(
       to_java_method_type(symbol.type), symbol.name, symbol_table);
+    set_declaring_class(symbol, arg0.get(ID_C_class));
 
     debug() << "Generating codet:  new opaque symbol: method '" << symbol.name
             << "'" << eom;

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -496,7 +496,7 @@ static void create_stub_global_symbol(
   new_symbol.name = symbol_id;
   new_symbol.base_name = symbol_basename;
   new_symbol.type = symbol_type;
-  new_symbol.type.set(ID_C_class, class_id);
+  set_declaring_class(new_symbol, class_id);
   // Public access is a guess; it encourages merging like-typed static fields,
   // whereas a more restricted visbility would encourage separating them.
   // Neither is correct, as without the class file we can't know the truth.

jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp

@@ -10,6 +10,7 @@ Author: Chris Smowton, chris.smowton@diffblue.com
 /// Unwind loops in static initializers
 
 #include "java_enum_static_init_unwind_handler.h"
+#include "java_utils.h"
 
 #include <util/invariant.h>
 #include <util/suffix.h>
@@ -76,11 +77,10 @@ tvt java_enum_static_init_unwind_handler(
     return tvt::unknown();
 
   const symbolt &function_symbol = symbol_table.lookup_ref(enum_function_id);
-  irep_idt class_id = function_symbol.type.get(ID_C_class);
-  INVARIANT(
-    !class_id.empty(), "functions should have their defining class annotated");
+  const auto class_id = declaring_class(function_symbol);
+  INVARIANT(class_id, "Java methods should have a defining class.");
 
-  const typet &class_type = symbol_table.lookup_ref(class_id).type;
+  const typet &class_type = symbol_table.lookup_ref(*class_id).type;
   size_t unwinds = class_type.get_size_t(ID_java_enum_static_unwind);
   if(unwinds != 0 && unwind_count < unwinds)
   {

jbmc/src/java_bytecode/java_static_initializers.cpp

@@ -232,7 +232,7 @@ static void clinit_wrapper_do_recursive_calls(
       symbol_table.symbols.end(),
       [&](const std::pair<irep_idt, symbolt> &symbol) {
         if(
-          symbol.second.type.get(ID_C_class) == class_name &&
+          declaring_class(symbol.second) == class_name &&
           symbol.second.is_static_lifetime &&
           !symbol.second.type.get_bool(ID_C_constant))
         {
@@ -352,10 +352,9 @@ static void create_clinit_wrapper_symbols(
   wrapper_method_symbol.pretty_name = wrapper_method_symbol.name;
   wrapper_method_symbol.base_name = "clinit_wrapper";
   wrapper_method_symbol.type = wrapper_method_type;
-  // Note this use of a type-comment to provide a back-link from a method
-  // to its associated class is the same one used in
-  // java_bytecode_convert_methodt::convert
-  wrapper_method_symbol.type.set(ID_C_class, class_name);
+  // This provides a back-link from a method to its associated class, as is done
+  // for java_bytecode_convert_methodt::convert.
+  set_declaring_class(wrapper_method_symbol, class_name);
   wrapper_method_symbol.mode = ID_java;
   bool failed = symbol_table.add(wrapper_method_symbol);
   INVARIANT(!failed, "clinit-wrapper symbol should be fresh");
@@ -453,21 +452,20 @@ code_blockt get_thread_safe_clinit_wrapper_body(
   message_handlert &message_handler)
 {
   const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
-  irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
-  INVARIANT(
-    !class_name.empty(), "wrapper function should be annotated with its class");
+  const auto class_name = declaring_class(wrapper_method_symbol);
+  INVARIANT(class_name, "Wrapper function should have an owning class.");
 
   const symbolt &clinit_state_sym =
-    symbol_table.lookup_ref(clinit_state_var_name(class_name));
+    symbol_table.lookup_ref(clinit_state_var_name(*class_name));
   const symbolt &clinit_thread_local_state_sym =
-    symbol_table.lookup_ref(clinit_thread_local_state_var_name(class_name));
+    symbol_table.lookup_ref(clinit_thread_local_state_var_name(*class_name));
 
   // Create a function-local variable "init_complete". This variable is used to
   // avoid inspecting the global state (clinit_state_sym) outside of
   // the critical-section.
   const symbolt &init_complete = add_new_variable_symbol(
     symbol_table,
-    clinit_local_init_complete_var_name(class_name),
+    clinit_local_init_complete_var_name(*class_name),
     bool_typet(),
     nil_exprt(),
     true,
@@ -598,7 +596,7 @@ code_blockt get_thread_safe_clinit_wrapper_body(
     code_blockt init_body;
     clinit_wrapper_do_recursive_calls(
       symbol_table,
-      class_name,
+      *class_name,
       init_body,
       nondet_static,
       object_factory_parameters,
@@ -666,12 +664,11 @@ code_ifthenelset get_clinit_wrapper_body(
   //   }
   // }
   const symbolt &wrapper_method_symbol = symbol_table.lookup_ref(function_id);
-  irep_idt class_name = wrapper_method_symbol.type.get(ID_C_class);
-  INVARIANT(
-    !class_name.empty(), "wrapper function should be annotated with its class");
+  const auto class_name = declaring_class(wrapper_method_symbol);
+  INVARIANT(class_name, "Wrapper function should have an owning class.");
 
   const symbolt &already_run_symbol =
-    symbol_table.lookup_ref(clinit_already_run_variable_name(class_name));
+    symbol_table.lookup_ref(clinit_already_run_variable_name(*class_name));
 
   equal_exprt check_already_run(
     already_run_symbol.symbol_expr(),
@@ -683,7 +680,7 @@ code_ifthenelset get_clinit_wrapper_body(
 
   clinit_wrapper_do_recursive_calls(
     symbol_table,
-    class_name,
+    *class_name,
     init_body,
     nondet_static,
     object_factory_parameters,
@@ -766,12 +763,9 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
       continue;
     }
 
-    const irep_idt class_id =
-      global_symbol.type.get(ID_C_class);
-    INVARIANT(
-      !class_id.empty(),
-      "static field should be annotated with its defining class");
-    stub_globals_by_class.insert({class_id, stub_global});
+    const auto class_id = declaring_class(global_symbol);
+    INVARIANT(class_id, "Static field should have a defining class.");
+    stub_globals_by_class.insert({*class_id, stub_global});
   }
 
   // For each distinct class that has stub globals, create a clinit symbol:
@@ -799,10 +793,9 @@ void stub_global_initializer_factoryt::create_stub_global_initializer_symbols(
     static_init_symbol.base_name = "clinit():V";
     static_init_symbol.mode = ID_java;
     static_init_symbol.type = thunk_type;
-    // Note this use of a type-comment to provide a back-link from a method
-    // to its associated class is the same one used in
-    // java_bytecode_convert_methodt::convert
-    static_init_symbol.type.set(ID_C_class, it->first);
+    // This provides a back-link from a method to its associated class, as is
+    // done for java_bytecode_convert_methodt::convert.
+    set_declaring_class(static_init_symbol, it->first);
 
     bool failed = symbol_table.add(static_init_symbol);
     INVARIANT(!failed, "symbol should not already exist");
@@ -839,17 +832,16 @@ code_blockt stub_global_initializer_factoryt::get_stub_initializer_body(
   message_handlert &message_handler)
 {
   const symbolt &stub_initializer_symbol = symbol_table.lookup_ref(function_id);
-  irep_idt class_id = stub_initializer_symbol.type.get(ID_C_class);
+  const auto class_id = declaring_class(stub_initializer_symbol);
   INVARIANT(
-    !class_id.empty(),
-    "synthetic static initializer should be annotated with its class");
+    class_id, "Synthetic static initializer should have an owning class.");
   code_blockt static_init_body;
 
   // Add a standard nondet initialisation for each global declared on this
   // class. Note this is the same invocation used in
   // java_static_lifetime_init.
 
-  auto class_globals = stub_globals_by_class.equal_range(class_id);
+  auto class_globals = stub_globals_by_class.equal_range(*class_id);
   INVARIANT(
     class_globals.first != class_globals.second,
     "class with synthetic clinit should have at least one global to init");

jbmc/src/java_bytecode/java_utils.cpp

@@ -464,3 +464,14 @@ symbolt &fresh_java_symbol(
   return get_fresh_aux_symbol(
     type, name_prefix, basename_prefix, source_location, ID_java, symbol_table);
 }
+
+optionalt<irep_idt> declaring_class(const symbolt &symbol)
+{
+  const irep_idt &class_id = symbol.type.get(ID_C_class);
+  return class_id.empty() ? optionalt<irep_idt>{} : class_id;
+}
+
+void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class)
+{
+  symbol.type.set(ID_C_class, declaring_class);
+}

jbmc/src/java_bytecode/java_utils.h

@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <unordered_set>
 
 #include <util/message.h>
+#include <util/optional.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
@@ -115,4 +116,14 @@ symbolt &fresh_java_symbol(
   const irep_idt &function_name,
   symbol_table_baset &symbol_table);
 
+/// Gets the identifier of the class which declared a given \p symbol. If the
+/// symbol is not declared by a class then an empty optional is returned. This
+/// is used for method symbols and static field symbols to link them back to the
+/// class which declared them.
+optionalt<irep_idt> declaring_class(const symbolt &symbol);
+
+/// Sets the identifier of the class which declared a given \p symbol to \p
+/// declaring_class.
+void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H

jbmc/src/jdiff/java_syntactic_diff.cpp

@@ -12,6 +12,7 @@ Author: Peter Schrammel
 #include "java_syntactic_diff.h"
 
 #include <goto-programs/goto_model.h>
+#include <java_bytecode/java_utils.h>
 
 bool java_syntactic_difft::operator()()
 {
@@ -35,16 +36,16 @@ bool java_syntactic_difft::operator()()
     CHECK_RETURN(fun1 != nullptr);
     const symbolt *fun2 = goto_model2.symbol_table.lookup(it->first);
     CHECK_RETURN(fun2 != nullptr);
-    const irep_idt &class_name = fun1->type.get(ID_C_class);
+    const optionalt<irep_idt> class_name = declaring_class(*fun1);
     bool function_access_changed =
       fun1->type.get(ID_access) != fun2->type.get(ID_access);
     bool class_access_changed = false;
     bool field_access_changed = false;
-    if(!class_name.empty())
+    if(class_name)
     {
-      const symbolt *class1 = goto_model1.symbol_table.lookup(class_name);
+      const symbolt *class1 = goto_model1.symbol_table.lookup(*class_name);
       CHECK_RETURN(class1 != nullptr);
-      const symbolt *class2 = goto_model2.symbol_table.lookup(class_name);
+      const symbolt *class2 = goto_model2.symbol_table.lookup(*class_name);
       CHECK_RETURN(class2 != nullptr);
       class_access_changed =
         class1->type.get(ID_access) != class2->type.get(ID_access);

jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp

@@ -12,6 +12,7 @@ Author: Diffblue Ltd.
 #include <algorithm>
 
 #include <java_bytecode/java_types.h>
+#include <java_bytecode/java_utils.h>
 #include <util/expr_iterator.h>
 
 /// Check the full tree of expr for any symbol_exprts that have an identifier id
@@ -37,6 +38,12 @@ SCENARIO(
     {
       REQUIRE(symbol_table.has_symbol("java::Parent1.x"));
     }
+    THEN("Static field 'Parent1.x' should be declared by class Parent1")
+    {
+      REQUIRE(
+        id2string(*declaring_class(
+          symbol_table.lookup_ref("java::Parent1.x"))) == "java::Parent1");
+    }
     THEN("No static field 'Test1.x' should be created")
     {
       REQUIRE(!symbol_table.has_symbol("java::Test1.x"));
@@ -62,6 +69,14 @@ SCENARIO(
     {
       REQUIRE(symbol_table.has_symbol("java::StaticInterface2.x"));
     }
+    THEN(
+      "Static field 'java::StaticInterface2.x' should be declared by "
+      "StaticInterface2")
+    {
+      REQUIRE(
+        id2string(*declaring_class(symbol_table.lookup_ref(
+          "java::StaticInterface2.x"))) == "java::StaticInterface2");
+    }
     THEN("No static field 'Test2.x' should be created")
     {
       REQUIRE(!symbol_table.has_symbol("java::Test2.x"));
@@ -93,6 +108,14 @@ SCENARIO(
     {
       REQUIRE(symbol_table.has_symbol("java::OpaqueParent3.x"));
     }
+    THEN(
+      "Static field 'OpaqueParent3.x' should be declared by class "
+      "OpaqueParent3")
+    {
+      REQUIRE(
+        id2string(*declaring_class(symbol_table.lookup_ref(
+          "java::OpaqueParent3.x"))) == "java::OpaqueParent3");
+    }
     THEN("No static field 'Test3.x' should be created")
     {
       REQUIRE(!symbol_table.has_symbol("java::Test3.x"));
@@ -124,6 +147,14 @@ SCENARIO(
     {
       REQUIRE(symbol_table.has_symbol("java::OpaqueInterface4.x"));
     }
+    THEN(
+      "Static field 'OpaqueInterface4.x' should be declared by class "
+      "OpaqueInterface4")
+    {
+      REQUIRE(
+        id2string(*declaring_class(symbol_table.lookup_ref(
+          "java::OpaqueInterface4.x"))) == "java::OpaqueInterface4");
+    }
     THEN("No static field 'Test4.x' should be created")
     {
       REQUIRE(!symbol_table.has_symbol("java::Test4.x"));
@@ -191,6 +222,12 @@ SCENARIO(
     {
       REQUIRE(symbol_table.has_symbol("java::Parent6.x"));
     }
+    THEN("Static field 'Parent6.x' should be declared by class Parent6")
+    {
+      REQUIRE(
+        id2string(*declaring_class(
+          symbol_table.lookup_ref("java::Parent6.x"))) == "java::Parent6");
+    }
     THEN("No static field 'Test6.x' should be created")
     {
       REQUIRE(!symbol_table.has_symbol("java::Test6.x"));
@@ -217,10 +254,26 @@ SCENARIO(
     {
       REQUIRE(symbol_table.has_symbol("java::otherpackage.Parent7.x"));
     }
+    THEN(
+      "Static field 'otherpackage.Parent7.x' should be declared by class "
+      "otherpackage.Parent7")
+    {
+      REQUIRE(
+        id2string(*declaring_class(symbol_table.lookup_ref(
+          "java::otherpackage.Parent7.x"))) == "java::otherpackage.Parent7");
+    }
     THEN("A static field StaticInterface7.x should exist")
     {
       REQUIRE(symbol_table.has_symbol("java::StaticInterface7.x"));
     }
+    THEN(
+      "Static field 'StaticInterface7.x' should be declared by class "
+      "StaticInterface7")
+    {
+      REQUIRE(
+        id2string(*declaring_class(symbol_table.lookup_ref(
+          "java::StaticInterface7.x"))) == "java::StaticInterface7");
+    }
     THEN("No static field 'Test7.x' should be created")
     {
       REQUIRE(!symbol_table.has_symbol("java::Test7.x"));
@@ -253,6 +306,12 @@ SCENARIO(
     {
       REQUIRE(symbol_table.has_symbol("java::Parent8.x"));
     }
+    THEN("Static field 'Parent8.x' should be declared by class Parent8")
+    {
+      REQUIRE(
+        id2string(*declaring_class(
+          symbol_table.lookup_ref("java::Parent8.x"))) == "java::Parent8");
+    }
     THEN("No static field 'Test8.x' should be created")
     {
       REQUIRE(!symbol_table.has_symbol("java::Test8.x"));
@@ -279,10 +338,22 @@ SCENARIO(
     {
       REQUIRE(symbol_table.has_symbol("java::Parent9.x"));
     }
+    THEN("Static field 'Parent9.x' should be declared by class Parent9")
+    {
+      REQUIRE(
+        id2string(*declaring_class(
+          symbol_table.lookup_ref("java::Parent9.x"))) == "java::Parent9");
+    }
     THEN("A static field StaticInterface9.x should exist")
     {
       REQUIRE(symbol_table.has_symbol("java::StaticInterface9.x"));
     }
+    THEN("Static field 'Parent8.x' should be declared by StaticInterface9")
+    {
+      REQUIRE(
+        id2string(*declaring_class(symbol_table.lookup_ref(
+          "java::StaticInterface9.x"))) == "java::StaticInterface9");
+    }
     THEN("No static field 'Test9.x' should be created")
     {
       REQUIRE(!symbol_table.has_symbol("java::Test9.x"));

jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.java

@@ -0,0 +1,5 @@
+public class ClassWithStaticMethod {
+  public static int staticFunc() {
+    return 0;
+  }
+}

jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp

@@ -8,11 +8,14 @@ Author: Diffblue Limited.
 
 #include <testing-utils/use_catch.h>
 
+#include <util/irep.h>
 #include <util/symbol_table.h>
 
 #include <java-testing-utils/load_java_class.h>
 #include <java-testing-utils/require_type.h>
 
+#include <java_bytecode/java_utils.h>
+
 SCENARIO(
   "java_bytecode_convert_bridge_method",
   "[core][java_bytecode][java_bytecode_convert_method]")
@@ -39,20 +42,29 @@ SCENARIO(
       {
         REQUIRE(function_type.get_bool(ID_is_bridge_method));
       }
+      THEN("The method should be marked as declared by its class")
+      {
+        REQUIRE(
+          id2string(*declaring_class(function_symbol)) ==
+          "java::ClassWithBridgeMethod");
+      }
     }
     WHEN("When parsing a non-bridge method")
-    {
-      THEN("THe method should not be marked as a bridge method")
     {
       const symbolt function_symbol =
         symbol_table.lookup_ref(method_name + ":(LClassWithBridgeMethod;)I");
 
       const java_method_typet &function_type =
         require_type::require_java_method(function_symbol.type);
-        THEN("The method should be marked as a bridge method")
+      THEN("The method should not be marked as a bridge method.")
       {
         REQUIRE_FALSE(function_type.get_bool(ID_is_bridge_method));
       }
+      THEN("The method should be marked as declared by its class")
+      {
+        REQUIRE(
+          id2string(*declaring_class(function_symbol)) ==
+          "java::ClassWithBridgeMethod");
       }
     }
   }
@@ -78,20 +90,29 @@ SCENARIO(
       {
         REQUIRE(to_java_method_type(function_type).get_native());
       }
+      THEN("The method should be marked as declared by its class")
+      {
+        REQUIRE(
+          id2string(*declaring_class(function_symbol)) ==
+          "java::ClassWithNativeMethod");
+      }
     }
     WHEN("When parsing a non-native method")
-    {
-      THEN("THe method should not be marked as a native method")
     {
       const symbolt function_symbol =
         symbol_table.lookup_ref(method_name + ":(I)Z");
 
       const java_method_typet &function_type =
         require_type::require_java_method(function_symbol.type);
-        THEN("The method should be marked as a native method")
+      THEN("The method should not be marked as a native method.")
       {
         REQUIRE_FALSE(to_java_method_type(function_type).get_native());
       }
+      THEN("The method should be marked as declared by its class")
+      {
+        REQUIRE(
+          id2string(*declaring_class(function_symbol)) ==
+          "java::ClassWithNativeMethod");
       }
     }
   }
@@ -116,6 +137,12 @@ SCENARIO(
       {
         REQUIRE(function_type.get_is_final());
       }
+      THEN("The method should be marked as declared by its class")
+      {
+        REQUIRE(
+          id2string(*declaring_class(function_symbol)) ==
+          "java::ClassWithFinalMethod");
+      }
     }
     WHEN("When parsing a non-final method")
     {
@@ -127,6 +154,12 @@ SCENARIO(
       {
         REQUIRE(!function_type.get_is_final());
       }
+      THEN("The method should be marked as declared by its class")
+      {
+        REQUIRE(
+          id2string(*declaring_class(function_symbol)) ==
+          "java::ClassWithFinalMethod");
+      }
     }
     WHEN("When parsing an opaque method")
     {
@@ -138,6 +171,11 @@ SCENARIO(
       {
         REQUIRE(function_type.get_is_final());
       }
+      THEN("The method should be marked as declared by its class")
+      {
+        REQUIRE(
+          id2string(*declaring_class(function_symbol)) == "java::OpaqueClass");
+      }
     }
   }
 }
@@ -161,6 +199,12 @@ SCENARIO(
       {
         REQUIRE(method_type.get_is_varargs());
       }
+      THEN("The method should be marked as declared by its class")
+      {
+        REQUIRE(
+          id2string(*declaring_class(method_symbol)) ==
+          "java::ClassWithVarArgsMethod");
+      }
     }
     WHEN("When parsing a method with constant number of arguments")
     {
@@ -172,6 +216,36 @@ SCENARIO(
       {
         REQUIRE_FALSE(method_type.get_is_varargs());
       }
+      THEN("The method should be marked as declared by its class")
+      {
+        REQUIRE(
+          id2string(*declaring_class(method_symbol)) ==
+          "java::ClassWithVarArgsMethod");
+      }
+    }
+  }
+}
+
+SCENARIO(
+  "java_bytecode_convert_static_method",
+  "[core][java_bytecode][java_bytecode_convert_method]")
+{
+  GIVEN("A class with a static method.")
+  {
+    const symbol_tablet symbol_table = load_java_class(
+      "ClassWithStaticMethod", "./java_bytecode/java_bytecode_convert_method");
+
+    WHEN("Parsing a static method.")
+    {
+      const symbolt method_symbol =
+        symbol_table.lookup_ref("java::ClassWithStaticMethod.staticFunc:()I");
+
+      THEN("The method should be marked as declared by its class")
+      {
+        REQUIRE(
+          id2string(*declaring_class(method_symbol)) ==
+          "java::ClassWithStaticMethod");
+      }
     }
   }
 }

jbmc/unit/java_bytecode/java_utils_test.cpp

@@ -368,3 +368,28 @@ SCENARIO("Test pretty printing auxiliary function", "[core][java_util_test]")
     }
   }
 }
+
+SCENARIO("Test symbol declarers.", "[core][java_util_test]")
+{
+  WHEN("We have a new symbol.")
+  {
+    symbolt symbol;
+
+    THEN("The symbol has no declarer.")
+    {
+      REQUIRE(!declaring_class(symbol).has_value());
+    }
+  }
+
+  WHEN("The declaring class of a symbol is set.")
+  {
+    const auto declaring_class = "java::java.lang.object";
+    symbolt symbol;
+    set_declaring_class(symbol, declaring_class);
+
+    THEN("Getting the declaring class of a symbol returns the class set.")
+    {
+      REQUIRE(id2string(*::declaring_class(symbol)) == declaring_class);
+    }
+  }
+}