From edc76d1c59ec36d9ccd30caca277ea9d612220a5 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 12 Feb 2020 14:27:03 +0000 Subject: [PATCH 1/3] Update parameter names These did not match their implementation names --- src/goto-programs/string_instrumentation.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) 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( From 51d792b4776ee20f930badff8d8df1133994c3ba Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 12 Feb 2020 16:55:56 +0000 Subject: [PATCH 2/3] Correct function_id comment The variable is used in the declaration of a variable. So there is no need to have the dud usage to suppress warnings about unused variables. Updated comment saying it was unused as well. --- jbmc/src/java_bytecode/java_string_library_preprocess.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index be406deb1c3..6fa8a2149ca 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,8 +1315,6 @@ 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; From 786f896685d7c88e61235d6320e612bb014b57bd Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 12 Feb 2020 16:56:34 +0000 Subject: [PATCH 3/3] Rename variable to self explantory name Makes clear it is what the function produces, and makes the comment explaining it redundant. --- .../java_bytecode/java_string_library_preprocess.cpp | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 6fa8a2149ca..c5a7569d739 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -1315,12 +1315,11 @@ code_blockt java_string_library_preprocesst::make_copy_constructor_code( const irep_idt &function_id, symbol_table_baset &symbol_table) { - // 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(); @@ -1328,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