Skip to content

Commit c4d79ab

Browse files
committed
Java string preprocessing: use provided source location
The code_returnt was previously generated without a source location, even though the containing function took one as an argument. That parameter, however, was not previously used.
1 parent c31edca commit c4d79ab

File tree

1 file changed

+5
-1
lines changed

1 file changed

+5
-1
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1836,7 +1836,11 @@ codet java_string_library_preprocesst::make_string_length_code(
18361836
symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
18371837
dereference_exprt deref=
18381838
checked_dereference(arg_this, arg_this.type().subtype());
1839-
return code_returnt(get_length(deref, symbol_table));
1839+
1840+
code_returnt ret(get_length(deref, symbol_table));
1841+
ret.add_source_location() = loc;
1842+
1843+
return ret;
18401844
}
18411845

18421846
bool java_string_library_preprocesst::implements_function(

0 commit comments

Comments
 (0)