Skip to content

Commit 49799cb

Browse files
author
Owen
committed
Fix wrong type for dereference expression #2
We should keep the struct tag type, not follow it and get the struct type
1 parent 96d572d commit 49799cb

File tree

1 file changed

+2
-10
lines changed

1 file changed

+2
-10
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 2 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -831,16 +831,8 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
831831
{
832832
PRECONDITION(implements_java_char_sequence_pointer(rhs.type()));
833833

834-
typet deref_type;
835-
if(rhs.type().subtype().id() == ID_struct_tag)
836-
deref_type =
837-
symbol_table
838-
.lookup_ref(to_struct_tag_type(rhs.type().subtype()).get_identifier())
839-
.type;
840-
else
841-
deref_type=rhs.type().subtype();
842-
843-
const dereference_exprt deref = checked_dereference(rhs, deref_type);
834+
const dereference_exprt deref =
835+
checked_dereference(rhs, rhs.type().subtype());
844836

845837
// Although we should not reach this code if rhs is null, the association
846838
// `pointer -> length` is added to the solver anyway, so we have to make sure

0 commit comments

Comments
 (0)