Merge pull request #4764 from diffblue/arraylength_fix

Daniel Kroening · web-flow · commit 891f04ed6e80 · 2019-06-09T11:34:25.000+01:00
fix for arraylength
diff --git 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);
 

Original file line number	Diff line number	Diff line change
`@@ -1603,8 +1603,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(`
`1603`	`1603`	`{`
`1604`	`1604`	`PRECONDITION(op.size() == 1 && results.size() == 1);`
`1605`	`1605`
`1606`		`- dereference_exprt array{`
`1607`		`- typecast_exprt{op[0], java_array_type(statement[0])}};`
	`1606`	`+ // any array type is fine here, so we go for a reference array`
	`1607`	`+ dereference_exprt array{typecast_exprt{op[0], java_array_type('a')}};`
`1608`	`1608`	`PRECONDITION(array.type().id() == ID_struct_tag);`
`1609`	`1609`	`array.set(ID_java_member_access, true);`
`1610`	`1610`