Skip to content

Commit 746e337

Browse files
Set mode of if_exprt introduced in preprocessing
A temporary variable is introduced later for this if_exprt and the mode needs to be known for the variable, other an invariant may fail.
1 parent 6b8583d commit 746e337

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

src/java_bytecode/java_string_library_preprocess.cpp

+2-1
Original file line numberDiff line numberDiff line change
@@ -902,10 +902,11 @@ void java_string_library_preprocesst::code_assign_java_string_to_string_expr(
902902
// Although we should not reach this code if rhs is null, the association
903903
// `pointer -> length` is added to the solver anyway, so we have to make sure
904904
// the length is set to something reasonable.
905-
const auto rhs_length = if_exprt(
905+
auto rhs_length = if_exprt(
906906
equal_exprt(rhs, null_pointer_exprt(to_pointer_type(rhs.type()))),
907907
from_integer(0, lhs.length().type()),
908908
get_length(deref, symbol_table));
909+
rhs_length.set(ID_mode, ID_java);
909910

910911
// Assignments
911912
code.add(code_assignt(lhs.length(), rhs_length), loc);

0 commit comments

Comments
 (0)