From 409d0fcc7683058e603f90c63a63d8daed436197 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 7 Jun 2019 12:56:00 +0100 Subject: [PATCH] fix for arraylength The type of the array for arraylength doesn't matter -- the previous implementation uses the first letter of the statement, which only happens to be a valid type character ('a'). --- jbmc/src/java_bytecode/java_bytecode_convert_method.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 8274e3f2227..9b3638b634d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -1603,8 +1603,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions( { PRECONDITION(op.size() == 1 && results.size() == 1); - dereference_exprt array{ - typecast_exprt{op[0], java_array_type(statement[0])}}; + // any array type is fine here, so we go for a reference array + dereference_exprt array{typecast_exprt{op[0], java_array_type('a')}}; PRECONDITION(array.type().id() == ID_struct_tag); array.set(ID_java_member_access, true);