Skip to content

Commit ecc0e43

Browse files
Document eval_is_upper_case
1 parent a345d30 commit ecc0e43

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

src/solvers/refinement/string_builtin_function.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -191,6 +191,11 @@ exprt string_set_char_builtin_functiont::length_constraint() const
191191

192192
static bool eval_is_upper_case(const mp_integer &c)
193193
{
194+
// Characters between 'A' and 'Z' are upper-case
195+
// Characters between 0xc0 (latin capital A with grave)
196+
// and 0xd6 (latin capital O with diaeresis) are upper-case
197+
// Characters between 0xd8 (latin capital O with stroke)
198+
// and 0xde (latin capital thorn) are upper-case
194199
return ('A' <= c && c <= 'Z') || (0xc0 <= c && c <= 0xd6) ||
195200
(0xd8 <= c && c <= 0xde);
196201
}

0 commit comments

Comments
 (0)