Skip to content

Commit db6b90e

Browse files
author
Daniel Kroening
committed
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').
1 parent bf5f7f7 commit db6b90e

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1603,8 +1603,9 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
16031603
{
16041604
PRECONDITION(op.size() == 1 && results.size() == 1);
16051605

1606+
// any array type is fine here, so we go for a reference array
16061607
dereference_exprt array{
1607-
typecast_exprt{op[0], java_array_type(statement[0])}};
1608+
typecast_exprt{op[0], java_array_type('a')}};
16081609
PRECONDITION(array.type().id() == ID_struct_tag);
16091610
array.set(ID_java_member_access, true);
16101611

0 commit comments

Comments
 (0)