diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 5f9e12e13e7..2eaed207f9b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1644,7 +1644,12 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method) symbol_table.lookup_ref(field_id).symbol_expr()); convert_getstatic( - arg0, symbol_expr, is_assertions_disabled_field, c, results); + i_it->source_location, + arg0, + symbol_expr, + is_assertions_disabled_field, + c, + results); } else if(bytecode == BC_putfield) { @@ -2649,6 +2654,7 @@ code_blockt java_bytecode_convert_methodt::convert_putfield( } void java_bytecode_convert_methodt::convert_getstatic( + const source_locationt &source_location, const exprt &arg0, const symbol_exprt &symbol_expr, const bool is_assertions_disabled_field, @@ -2676,7 +2682,9 @@ void java_bytecode_convert_methodt::convert_getstatic( needed_lazy_methods->add_needed_class(arg0.get_string(ID_class)); } } - results[0] = java_bytecode_promotion(symbol_expr); + symbol_exprt symbol_with_location = symbol_expr; + symbol_with_location.add_source_location() = source_location; + results[0] = java_bytecode_promotion(symbol_with_location); // Note this initializer call deliberately inits the class used to make // the reference, which may be a child of the class that actually defines diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h index 5f315c5c208..5d5d300f9f6 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h @@ -432,6 +432,7 @@ class java_bytecode_convert_methodt:public messaget exprt::operandst &results) const; void convert_getstatic( + const source_locationt &source_location, const exprt &arg0, const symbol_exprt &symbol_expr, bool is_assertions_disabled_field, diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassReadingStaticField.class b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassReadingStaticField.class new file mode 100644 index 00000000000..0fb10a2594f Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassReadingStaticField.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassReadingStaticField.java b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassReadingStaticField.java new file mode 100644 index 00000000000..548dd708578 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/ClassReadingStaticField.java @@ -0,0 +1,11 @@ +public class ClassReadingStaticField { + + static int x; + + public static int test() { + + return x; + + } + +} 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 c3ca17c47cf..39eb3dee2fc 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 @@ -291,6 +291,45 @@ SCENARIO( } } +SCENARIO( + "java_bytecode_convert_method_with_getstatic", + "[core][java_bytecode][java_bytecode_convert_method]") +{ + GIVEN("A class that reads a static field.") + { + const symbol_tablet symbol_table = load_java_class( + "ClassReadingStaticField", + "./java_bytecode/java_bytecode_convert_method"); + + WHEN("Converting the method that reads said field") + { + const auto &method_symbol = + symbol_table.lookup_ref("java::ClassReadingStaticField.test:()I"); + + THEN( + "There should be a symbol expression attributed to bytecode index " + "0 (the getstatic instruction)") + { + bool found = false; + method_symbol.value.visit_pre([&found](const exprt &subexpr) { + if( + const auto symbol_expr = + expr_try_dynamic_cast(subexpr)) + { + if( + symbol_expr->source_location().get_java_bytecode_index() == "0" && + symbol_expr->get_identifier() == + "java::ClassReadingStaticField.x") + found = true; + } + }); + + REQUIRE(found); + } + } + } +} + /// Allow access to private methods so that they can be unit tested class java_bytecode_convert_method_unit_testt {