diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index be406deb1c3..c5a7569d739 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1300,7 +1300,8 @@ code_blockt java_string_library_preprocesst::make_copy_string_code( /// object. /// \param type: type of the function /// \param loc: location in the source -/// \param function_id: unused +/// \param function_id: name of the function (used for variable naming) where +/// the generated code ends up. /// \param symbol_table: symbol table /// \return Code corresponding to: /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1314,14 +1315,11 @@ code_blockt java_string_library_preprocesst::make_copy_constructor_code( const irep_idt &function_id, symbol_table_baset &symbol_table) { - (void)function_id; - - // Code for the output - code_blockt code; + code_blockt copy_constructor_body; // String expression that will hold the result const refined_string_exprt string_expr = - decl_string_expr(loc, function_id, symbol_table, code); + decl_string_expr(loc, function_id, symbol_table, copy_constructor_body); // Assign argument to a string_expr const java_method_typet::parameterst ¶ms = type.parameters(); @@ -1329,16 +1327,16 @@ code_blockt java_string_library_preprocesst::make_copy_constructor_code( PRECONDITION(!params[1].get_identifier().empty()); const symbol_exprt arg1{params[1].get_identifier(), params[1].type()}; code_assign_java_string_to_string_expr( - string_expr, arg1, loc, symbol_table, code); + string_expr, arg1, loc, symbol_table, copy_constructor_body); // Assign string_expr to `this` object const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()}; - code.add( + copy_constructor_body.add( code_assign_string_expr_to_java_string( arg_this, string_expr, symbol_table, true), loc); - return code; + return copy_constructor_body; } /// Generates code for the String.length method diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp index 5ad323737bc..f01c8732779 100644 --- a/src/goto-programs/string_instrumentation.cpp +++ b/src/goto-programs/string_instrumentation.cpp @@ -78,16 +78,16 @@ class string_instrumentationt:public messaget } void instrument(goto_programt &dest, goto_programt::targett it); - void do_function_call(goto_programt &dest, goto_programt::targett it); + void do_function_call(goto_programt &dest, goto_programt::targett target); // strings void do_sprintf( goto_programt &dest, - goto_programt::targett it, + goto_programt::targett target, const code_function_callt &); void do_snprintf( goto_programt &dest, - goto_programt::targett it, + goto_programt::targett target, const code_function_callt &); void do_strcat( goto_programt &dest, @@ -99,19 +99,19 @@ class string_instrumentationt:public messaget const code_function_callt &); void do_strchr( goto_programt &dest, - goto_programt::targett it, + goto_programt::targett target, const code_function_callt &); void do_strrchr( goto_programt &dest, - goto_programt::targett it, + goto_programt::targett target, const code_function_callt &); void do_strstr( goto_programt &dest, - goto_programt::targett it, + goto_programt::targett target, const code_function_callt &); void do_strtok( goto_programt &dest, - goto_programt::targett it, + goto_programt::targett target, const code_function_callt &); void do_strerror( goto_programt &dest, @@ -119,7 +119,7 @@ class string_instrumentationt:public messaget const code_function_callt &); void do_fscanf( goto_programt &dest, - goto_programt::targett it, + goto_programt::targett target, const code_function_callt &); void do_format_string_read(