diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 3241a20fbb7..5580caa8862 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/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)+ diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 9aae017a6e7..f1b5fe03e2d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/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 ¶meters = 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; diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index 4c895d2a3da..a1450e0e7ba 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/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. diff --git a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp b/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp index bbdc9c92532..904e2785bbd 100644 --- a/jbmc/src/java_bytecode/java_enum_static_init_unwind_handler.cpp +++ b/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 #include @@ -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) { diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp index 051ad245b4d..0c8c8221901 100644 --- a/jbmc/src/java_bytecode/java_static_initializers.cpp +++ b/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 &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"); diff --git a/jbmc/src/java_bytecode/java_utils.cpp b/jbmc/src/java_bytecode/java_utils.cpp index 1dfdfb878df..91f9e2a4dbb 100644 --- a/jbmc/src/java_bytecode/java_utils.cpp +++ b/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 declaring_class(const symbolt &symbol) +{ + const irep_idt &class_id = symbol.type.get(ID_C_class); + return class_id.empty() ? optionalt{} : class_id; +} + +void set_declaring_class(symbolt &symbol, const irep_idt &declaring_class) +{ + symbol.type.set(ID_C_class, declaring_class); +} diff --git a/jbmc/src/java_bytecode/java_utils.h b/jbmc/src/java_bytecode/java_utils.h index 0f4b38a9623..d2eddf81a10 100644 --- a/jbmc/src/java_bytecode/java_utils.h +++ b/jbmc/src/java_bytecode/java_utils.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -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 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 diff --git a/jbmc/src/jdiff/java_syntactic_diff.cpp b/jbmc/src/jdiff/java_syntactic_diff.cpp index b99707a1f4c..bc436f691a7 100644 --- a/jbmc/src/jdiff/java_syntactic_diff.cpp +++ b/jbmc/src/jdiff/java_syntactic_diff.cpp @@ -12,6 +12,7 @@ Author: Peter Schrammel #include "java_syntactic_diff.h" #include +#include 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 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); diff --git a/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp b/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp index fe32f90b8bf..a505fed318e 100644 --- a/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp +++ b/jbmc/unit/java_bytecode/inherited_static_fields/inherited_static_fields.cpp @@ -12,6 +12,7 @@ Author: Diffblue Ltd. #include #include +#include #include /// 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")); diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.class b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.class new file mode 100644 index 00000000000..93e79e8b5dc Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.java b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.java new file mode 100644 index 00000000000..e70df5f7e10 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassWithStaticMethod.java @@ -0,0 +1,5 @@ +public class ClassWithStaticMethod { + public static int staticFunc() { + return 0; + } +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp index b4539c8f0e1..dbe50f0523f 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_method.cpp @@ -8,11 +8,14 @@ Author: Diffblue Limited. #include +#include #include #include #include +#include + 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 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") - { - REQUIRE_FALSE(function_type.get_bool(ID_is_bridge_method)); - } + const java_method_typet &function_type = + require_type::require_java_method(function_symbol.type); + 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 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") - { - REQUIRE_FALSE(to_java_method_type(function_type).get_native()); - } + const java_method_typet &function_type = + require_type::require_java_method(function_symbol.type); + 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"); + } } } } diff --git a/jbmc/unit/java_bytecode/java_utils_test.cpp b/jbmc/unit/java_bytecode/java_utils_test.cpp index d56a08323fd..3bee7b0c05d 100644 --- a/jbmc/unit/java_bytecode/java_utils_test.cpp +++ b/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); + } + } +}