From c4d79ab2379c147fee756b158c501b68a6ea8d0f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 13 Aug 2018 11:51:44 +0000 Subject: [PATCH] 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. --- jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index e7c8c8058c7..76b019cd3a2 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1836,7 +1836,11 @@ codet java_string_library_preprocesst::make_string_length_code( symbol_exprt arg_this(params[0].get_identifier(), params[0].type()); dereference_exprt deref= checked_dereference(arg_this, arg_this.type().subtype()); - return code_returnt(get_length(deref, symbol_table)); + + code_returnt ret(get_length(deref, symbol_table)); + ret.add_source_location() = loc; + + return ret; } bool java_string_library_preprocesst::implements_function(