diff --git a/jbmc/src/java_bytecode/java_local_variable_table.cpp b/jbmc/src/java_bytecode/java_local_variable_table.cpp index 28c0731ec09..9d44666f636 100644 --- a/jbmc/src/java_bytecode/java_local_variable_table.cpp +++ b/jbmc/src/java_bytecode/java_local_variable_table.cpp @@ -768,9 +768,20 @@ void java_bytecode_convert_methodt::setup_local_variables( << " name " << v.var.name << " v.var.descriptor '" << v.var.descriptor << "' holes " << v.holes.size() << eom; #endif - typet t; - // TODO: might need changing once descriptor/signature issue is resolved - t=java_type_from_string(v.var.descriptor); + + const std::string &method_name = id2string(method_id); + const size_t method_name_end = method_name.rfind(":("); + const size_t class_name_end = method_name.rfind('.', method_name_end); + INVARIANT( + method_name_end != std::string::npos && + class_name_end != std::string::npos, + "A method name has the format class `.` method `:(`signature`)`."); + const std::string class_name = method_name.substr(0, class_name_end); + + const typet t = v.var.signature.has_value() + ? java_type_from_string_with_exception( + v.var.descriptor, v.var.signature, class_name) + : java_type_from_string(v.var.descriptor); std::ostringstream id_oss; id_oss << method_id << "::" << v.var.start_pc << "::" << v.var.name; diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 5bf5f13742e..b38b34278a7 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -33,6 +33,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ java_bytecode/java_bytecode_parse_generics/parse_nested_generics.cpp \ java_bytecode/java_bytecode_parse_generics/parse_recursive_generic_class.cpp \ java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp \ + java_bytecode/java_bytecode_parse_generics/parse_lvtt_generic_local_vars.cpp \ java_bytecode/java_bytecode_parse_lambdas/java_bytecode_convert_class_lambda_method_handles.cpp \ java_bytecode/java_bytecode_parse_lambdas/java_bytecode_parse_lambda_method_table.cpp \ java_bytecode/java_bytecode_parser/parse_java_annotations.cpp \ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericLocalVar.class b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericLocalVar.class new file mode 100644 index 00000000000..c51cc425753 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericLocalVar.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericLocalVar.java b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericLocalVar.java new file mode 100644 index 00000000000..f392397334d --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericLocalVar.java @@ -0,0 +1,5 @@ +public class GenericLocalVar { + public void f() { + java.util.ArrayList l = null; + } +} diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_lvtt_generic_local_vars.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_lvtt_generic_local_vars.cpp new file mode 100644 index 00000000000..89b3811d53c --- /dev/null +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_lvtt_generic_local_vars.cpp @@ -0,0 +1,35 @@ +/*******************************************************************\ + + Module: Unit tests for parsing generic local variables from the LVTT + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include + +SCENARIO( + "parse_lvtt_generic_local_vars", + "[core][java_bytecode][java_bytecode_parse_generics]") +{ + const symbol_tablet &new_symbol_table = load_java_class( + "GenericLocalVar", "./java_bytecode/java_bytecode_parse_generics"); + + const std::string var_name("java::GenericLocalVar.f:()V::1::l"); + REQUIRE(new_symbol_table.has_symbol(var_name)); + + WHEN("Local variable has an entry in the LVTT") + { + THEN("The type should be generic and instantiated with Double") + { + const symbolt &var_symbol = new_symbol_table.lookup_ref(var_name); + java_generic_typet local_var_type = + require_type::require_java_generic_type( + var_symbol.type, + {{require_type::type_argument_kindt::Inst, + "java::java.lang.Double"}}); + } + } +}