Skip to content

Commit 8aee75f

Browse files
committed
C library: add __tolower as alternative name for tolower
macOS eventually calls a function called `__tolower`. Rename our previous implementation to `__CPROVER_tolower` and make both `tolower` and `__tolower` use this. Also enable the regression test of it.
1 parent f18b509 commit 8aee75f

File tree

4 files changed

+27
-4
lines changed

4 files changed

+27
-4
lines changed

regression/cbmc-library/tolower-01/main.c

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,8 @@
33

44
int main()
55
{
6-
tolower();
7-
assert(0);
6+
int x;
7+
int r = tolower(x);
8+
assert(r >= x);
89
return 0;
910
}

regression/cbmc-library/tolower-01/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
main.c
33
--pointer-check --bounds-check
44
^EXIT=0$

src/ansi-c/library/ctype.c

Lines changed: 21 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -95,10 +95,30 @@ int isupper(int c)
9595
int isxdigit(int c)
9696
{ return (c>='A' && c<='F') || (c>='a' && c<='f') || (c>='0' && c<='9'); }
9797

98+
/* FUNCTION: __CPROVER_tolower */
99+
100+
int __CPROVER_tolower(int c)
101+
{
102+
return (c >= 'A' && c <= 'Z') ? c + ('a' - 'A') : c;
103+
}
104+
98105
/* FUNCTION: tolower */
99106

107+
int __CPROVER_tolower(int c);
108+
100109
int tolower(int c)
101-
{ return (c>='A' && c<='Z')?c+('a'-'A'):c; }
110+
{
111+
return __CPROVER_tolower(c);
112+
}
113+
114+
/* FUNCTION: __tolower */
115+
116+
int __CPROVER_tolower(int c);
117+
118+
int __tolower(int c)
119+
{
120+
return __CPROVER_tolower(c);
121+
}
102122

103123
/* FUNCTION: toupper */
104124

src/ansi-c/library_check.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,9 +54,11 @@ perl -p -i -e 's/^__stdio_common_vsprintf\n//' __functions # snprintf, Windows
5454
perl -p -i -e 's/^__stdio_common_vsscanf\n//' __functions # sscanf, Windows
5555
perl -p -i -e 's/^__srget\n//' __functions # gets, FreeBSD
5656
perl -p -i -e 's/^__swbuf\n//' __functions # putc, FreeBSD
57+
perl -p -i -e 's/^__tolower\n//' __functions # tolower, macOS
5758

5859
# Some functions are covered by existing tests:
5960
perl -p -i -e 's/^__CPROVER_(creat|fcntl|open|openat)\n//' __functions # creat, fcntl, open, openat
61+
perl -p -i -e 's/^__CPROVER_tolower\n//' __functions # tolower
6062
perl -p -i -e 's/^(creat|fcntl|open|openat)64\n//' __functions # same as creat, fcntl, open, openat
6163
perl -p -i -e 's/^__CPROVER_deallocate\n//' __functions # free-01
6264
perl -p -i -e 's/^__builtin_alloca\n//' __functions # alloca-01

0 commit comments

Comments
 (0)