Skip to content

Commit 00af153

Browse files
author
Lukasz A.J. Wrona
committed
Add comment on implementation status of String.replace
1 parent f2fab1a commit 00af153

File tree

1 file changed

+8
-4
lines changed

1 file changed

+8
-4
lines changed

src/solvers/refinement/string_constraint_generator_transformation.cpp

+8-4
Original file line numberDiff line numberDiff line change
@@ -384,10 +384,14 @@ static optionalt<std::pair<exprt, exprt>> to_char_pair(
384384
return { };
385385
}
386386

387-
/// add axioms corresponding to the String.replace java function
388-
/// \par parameters: function application with three arguments, the first is a
389-
/// string,
390-
/// the second and the third are either pair of characters or a pair of strings
387+
/// Add axioms corresponding to the String.replace java function
388+
/// Only supports String.replace(char, char) and
389+
/// String.replace(String, String) for single-character strings
390+
/// Returns original string in every other case (that behaviour is to
391+
/// be fixed in the future)
392+
/// \param f function application with three arguments, the first is a
393+
/// string, the second and the third are either pair of characters or
394+
/// a pair of strings
391395
/// \return a new string expression
392396
string_exprt string_constraint_generatort::add_axioms_for_replace(
393397
const function_application_exprt &f)

0 commit comments

Comments
 (0)