Skip to content

Commit aa5dac2

Browse files
author
Thomas Kiley
authored
Merge pull request #5232 from thk123/misc-string-cleanup
Misc string cleanup
2 parents a3c58a4 + 786f896 commit aa5dac2

File tree

2 files changed

+15
-17
lines changed

2 files changed

+15
-17
lines changed

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

+7-9
Original file line numberDiff line numberDiff line change
@@ -1300,7 +1300,8 @@ code_blockt java_string_library_preprocesst::make_copy_string_code(
13001300
/// object.
13011301
/// \param type: type of the function
13021302
/// \param loc: location in the source
1303-
/// \param function_id: unused
1303+
/// \param function_id: name of the function (used for variable naming) where
1304+
/// the generated code ends up.
13041305
/// \param symbol_table: symbol table
13051306
/// \return Code corresponding to:
13061307
/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1314,31 +1315,28 @@ code_blockt java_string_library_preprocesst::make_copy_constructor_code(
13141315
const irep_idt &function_id,
13151316
symbol_table_baset &symbol_table)
13161317
{
1317-
(void)function_id;
1318-
1319-
// Code for the output
1320-
code_blockt code;
1318+
code_blockt copy_constructor_body;
13211319

13221320
// String expression that will hold the result
13231321
const refined_string_exprt string_expr =
1324-
decl_string_expr(loc, function_id, symbol_table, code);
1322+
decl_string_expr(loc, function_id, symbol_table, copy_constructor_body);
13251323

13261324
// Assign argument to a string_expr
13271325
const java_method_typet::parameterst &params = type.parameters();
13281326
PRECONDITION(!params[0].get_identifier().empty());
13291327
PRECONDITION(!params[1].get_identifier().empty());
13301328
const symbol_exprt arg1{params[1].get_identifier(), params[1].type()};
13311329
code_assign_java_string_to_string_expr(
1332-
string_expr, arg1, loc, symbol_table, code);
1330+
string_expr, arg1, loc, symbol_table, copy_constructor_body);
13331331

13341332
// Assign string_expr to `this` object
13351333
const symbol_exprt arg_this{params[0].get_identifier(), params[0].type()};
1336-
code.add(
1334+
copy_constructor_body.add(
13371335
code_assign_string_expr_to_java_string(
13381336
arg_this, string_expr, symbol_table, true),
13391337
loc);
13401338

1341-
return code;
1339+
return copy_constructor_body;
13421340
}
13431341

13441342
/// Generates code for the String.length method

src/goto-programs/string_instrumentation.cpp

+8-8
Original file line numberDiff line numberDiff line change
@@ -78,16 +78,16 @@ class string_instrumentationt:public messaget
7878
}
7979

8080
void instrument(goto_programt &dest, goto_programt::targett it);
81-
void do_function_call(goto_programt &dest, goto_programt::targett it);
81+
void do_function_call(goto_programt &dest, goto_programt::targett target);
8282

8383
// strings
8484
void do_sprintf(
8585
goto_programt &dest,
86-
goto_programt::targett it,
86+
goto_programt::targett target,
8787
const code_function_callt &);
8888
void do_snprintf(
8989
goto_programt &dest,
90-
goto_programt::targett it,
90+
goto_programt::targett target,
9191
const code_function_callt &);
9292
void do_strcat(
9393
goto_programt &dest,
@@ -99,27 +99,27 @@ class string_instrumentationt:public messaget
9999
const code_function_callt &);
100100
void do_strchr(
101101
goto_programt &dest,
102-
goto_programt::targett it,
102+
goto_programt::targett target,
103103
const code_function_callt &);
104104
void do_strrchr(
105105
goto_programt &dest,
106-
goto_programt::targett it,
106+
goto_programt::targett target,
107107
const code_function_callt &);
108108
void do_strstr(
109109
goto_programt &dest,
110-
goto_programt::targett it,
110+
goto_programt::targett target,
111111
const code_function_callt &);
112112
void do_strtok(
113113
goto_programt &dest,
114-
goto_programt::targett it,
114+
goto_programt::targett target,
115115
const code_function_callt &);
116116
void do_strerror(
117117
goto_programt &dest,
118118
goto_programt::targett it,
119119
const code_function_callt &);
120120
void do_fscanf(
121121
goto_programt &dest,
122-
goto_programt::targett it,
122+
goto_programt::targett target,
123123
const code_function_callt &);
124124

125125
void do_format_string_read(

0 commit comments

Comments
 (0)