Skip to content

Commit 5ae5be9

Browse files
fixup! Add string_to_upper_case_builtin_functiont constructor
1 parent 39218ae commit 5ae5be9

File tree

2 files changed

+2
-6
lines changed

2 files changed

+2
-6
lines changed

src/solvers/refinement/string_builtin_function.cpp

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -410,18 +410,14 @@ optionalt<exprt> string_to_upper_case_builtin_functiont::eval(
410410
return make_string(input_opt.value(), type);
411411
}
412412

413-
/// Set of constranits ensuring `result` corresponds to `input` in which
413+
/// Set of constraints ensuring `result` corresponds to `input` in which
414414
/// lowercase characters of Basic Latin and Latin-1 supplement of unicode
415415
/// have been converted to uppercase. These constraints are:
416416
/// 1. res.length = str.length && return_code = 0
417417
/// 2. forall i < str.length.
418418
/// is_lower_case(str[i]) ? res[i] = str[i] - 0x20 : res[i] = str[i]
419419
///
420420
/// \param fresh_symbol: generator of fresh symbols
421-
/// \param res: array of characters expression
422-
/// \param str: array of characters expression
423-
/// \return integer expression which is different from `0` when there is an
424-
/// exception to signal
425421
string_constraintst string_to_upper_case_builtin_functiont::constraints(
426422
symbol_generatort &fresh_symbol) const
427423
{

src/solvers/refinement/string_builtin_function.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -251,7 +251,7 @@ class string_to_upper_case_builtin_functiont
251251

252252
string_constraintst constraints(class symbol_generatort &fresh_symbol) const;
253253

254-
/// \copydoc constraints(class symbol_generatort&)
254+
/// \copydoc constraints(symbol_generatort&)
255255
string_constraintst
256256
constraints(string_constraint_generatort &generator) const override
257257
{

0 commit comments

Comments
 (0)