Merge pull request #8283 from tautschnig/features/tolower

C library: add __to{lower,upper} as alternative names for {tolower,toupper}

Author: kroening

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

@@ -3,7 +3,8 @@
 
 int main()
 {
-  tolower();
-  assert(0);
+  int x;
+  int r = tolower(x);
+  assert(r >= x);
   return 0;
 }

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

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

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

@@ -3,7 +3,8 @@
 
 int main()
 {
-  toupper();
-  assert(0);
+  int x;
+  int r = toupper(x);
+  assert(r <= x);
   return 0;
 }

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

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

src/ansi-c/library/ctype.c

@@ -95,12 +95,52 @@ int isupper(int c)
 int isxdigit(int c)
 { return (c>='A' && c<='F') || (c>='a' && c<='f') || (c>='0' && c<='9'); }
 
+/* FUNCTION: __CPROVER_tolower */
+
+int __CPROVER_tolower(int c)
+{
+  return (c >= 'A' && c <= 'Z') ? c + ('a' - 'A') : c;
+}
+
 /* FUNCTION: tolower */
 
+int __CPROVER_tolower(int c);
+
 int tolower(int c)
-{ return (c>='A' && c<='Z')?c+('a'-'A'):c; }
+{
+  return __CPROVER_tolower(c);
+}
+
+/* FUNCTION: __tolower */
+
+int __CPROVER_tolower(int c);
+
+int __tolower(int c)
+{
+  return __CPROVER_tolower(c);
+}
+
+/* FUNCTION: __CPROVER_toupper */
+
+int __CPROVER_toupper(int c)
+{
+  return (c >= 'a' && c <= 'z') ? c - ('a' - 'A') : c;
+}
 
 /* FUNCTION: toupper */
 
+int __CPROVER_toupper(int c);
+
 int toupper(int c)
-{ return (c>='a' && c<='z')?c-('a'-'A'):c; }
+{
+  return __CPROVER_toupper(c);
+}
+
+/* FUNCTION: __toupper */
+
+int __CPROVER_toupper(int c);
+
+int __toupper(int c)
+{
+  return __CPROVER_toupper(c);
+}

src/ansi-c/library_check.sh

@@ -54,9 +54,12 @@ perl -p -i -e 's/^__stdio_common_vsprintf\n//' __functions # snprintf, Windows
 perl -p -i -e 's/^__stdio_common_vsscanf\n//' __functions # sscanf, Windows
 perl -p -i -e 's/^__srget\n//' __functions # gets, FreeBSD
 perl -p -i -e 's/^__swbuf\n//' __functions # putc, FreeBSD
+perl -p -i -e 's/^__tolower\n//' __functions # tolower, macOS
+perl -p -i -e 's/^__toupper\n//' __functions # toupper, macOS
 
 # Some functions are covered by existing tests:
 perl -p -i -e 's/^__CPROVER_(creat|fcntl|open|openat)\n//' __functions # creat, fcntl, open, openat
+perl -p -i -e 's/^__CPROVER_(tolower|toupper)\n//' __functions # tolower, toupper
 perl -p -i -e 's/^(creat|fcntl|open|openat)64\n//' __functions # same as creat, fcntl, open, openat
 perl -p -i -e 's/^__CPROVER_deallocate\n//' __functions # free-01
 perl -p -i -e 's/^__builtin_alloca\n//' __functions # alloca-01