Skip to content

Misc string cleanup #5232

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Feb 21, 2020
Merged

Misc string cleanup #5232

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
edc76d1
Update parameter names
Feb 12, 2020
51d792b
Correct function_id comment
Feb 12, 2020
786f896
Rename variable to self explantory name
Feb 12, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 7 additions & 9 deletions jbmc/src/java_bytecode/java_string_library_preprocess.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Expand All @@ -1314,31 +1315,28 @@ 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 &params = type.parameters();
PRECONDITION(!params[0].get_identifier().empty());
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
Expand Down
16 changes: 8 additions & 8 deletions src/goto-programs/string_instrumentation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -99,27 +99,27 @@ 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,
goto_programt::targett it,
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(
Expand Down