From fd9375b3ac0018f23842e41bafd42813d4950afc Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 3 Feb 2021 09:49:41 +0100
Subject: [PATCH] [Libc] add spec for wcscasecmp
---
share/libc/wchar.h | 7 +++++++
.../tests/known/oracle/printf.res.oracle | 12 ++++++------
.../tests/known/oracle/swprintf.res.oracle | 12 ++++++------
.../variadic/tests/known/oracle/wchar.res.oracle | 12 ++++++------
tests/libc/oracle/fc_libc.0.res.oracle | 14 +++++++-------
tests/libc/oracle/fc_libc.1.res.oracle | 8 ++++++++
tests/libc/oracle/wchar_h.res.oracle | 16 ++++++++++++++++
tests/libc/wchar_h.c | 3 +++
8 files changed, 59 insertions(+), 25 deletions(-)
diff --git a/share/libc/wchar.h b/share/libc/wchar.h
index 5ea6aa80e83..bb8a4b6fd45 100644
--- a/share/libc/wchar.h
+++ b/share/libc/wchar.h
@@ -260,6 +260,13 @@ extern wchar_t *fgetws(wchar_t * restrict ws, int n, FILE * restrict stream);
}
*/
+/*@
+ requires valid_wstring_ws1: valid_read_wstring(ws1);
+ requires valid_wstring_ws2: valid_read_wstring(ws2);
+ assigns \result \from indirect:ws1[0..], indirect:ws2[0..];
+*/
+extern int wcscasecmp(const wchar_t *ws1, const wchar_t *ws2);
+
/* It is unclear whether these are more often in wchar.h or stdio.h */
extern int fwprintf(FILE * stream, const wchar_t * format, ...);
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index cac34c3b811..b8b4149310d 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:265:
+[variadic] FRAMAC_SHARE/libc/wchar.h:272:
Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:267:
+[variadic] FRAMAC_SHARE/libc/wchar.h:274:
Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:269:
+[variadic] FRAMAC_SHARE/libc/wchar.h:276:
Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:272:
+[variadic] FRAMAC_SHARE/libc/wchar.h:279:
Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:274:
+[variadic] FRAMAC_SHARE/libc/wchar.h:281:
Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:276:
+[variadic] FRAMAC_SHARE/libc/wchar.h:283:
Declaration of variadic function swscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
diff --git a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
index 505fe9d8346..326508d6ec1 100644
--- a/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/swprintf.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:265:
+[variadic] FRAMAC_SHARE/libc/wchar.h:272:
Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:267:
+[variadic] FRAMAC_SHARE/libc/wchar.h:274:
Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:269:
+[variadic] FRAMAC_SHARE/libc/wchar.h:276:
Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:272:
+[variadic] FRAMAC_SHARE/libc/wchar.h:279:
Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:274:
+[variadic] FRAMAC_SHARE/libc/wchar.h:281:
Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:276:
+[variadic] FRAMAC_SHARE/libc/wchar.h:283:
Declaration of variadic function swscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
diff --git a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
index b0188cdf152..fb03056d82e 100644
--- a/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/wchar.res.oracle
@@ -1,14 +1,14 @@
-[variadic] FRAMAC_SHARE/libc/wchar.h:265:
+[variadic] FRAMAC_SHARE/libc/wchar.h:272:
Declaration of variadic function fwprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:267:
+[variadic] FRAMAC_SHARE/libc/wchar.h:274:
Declaration of variadic function swprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:269:
+[variadic] FRAMAC_SHARE/libc/wchar.h:276:
Declaration of variadic function wprintf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:272:
+[variadic] FRAMAC_SHARE/libc/wchar.h:279:
Declaration of variadic function wscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:274:
+[variadic] FRAMAC_SHARE/libc/wchar.h:281:
Declaration of variadic function fwscanf.
-[variadic] FRAMAC_SHARE/libc/wchar.h:276:
+[variadic] FRAMAC_SHARE/libc/wchar.h:283:
Declaration of variadic function swscanf.
[variadic] FRAMAC_SHARE/libc/stdio.h:207:
Declaration of variadic function fprintf.
diff --git a/tests/libc/oracle/fc_libc.0.res.oracle b/tests/libc/oracle/fc_libc.0.res.oracle
index 9cd8d6f3657..dadf77c4d5a 100644
--- a/tests/libc/oracle/fc_libc.0.res.oracle
+++ b/tests/libc/oracle/fc_libc.0.res.oracle
@@ -43,7 +43,7 @@
wcscpy (0 call); wcslen (2 calls); wcsncat (0 call); wcsncpy (0 call);
wmemcpy (0 call); wmemset (0 call);
- Specified-only functions (413)
+ Specified-only functions (414)
==============================
FD_CLR (0 call); FD_ISSET (0 call); FD_SET (0 call); FD_ZERO (0 call);
Frama_C_int_interval (0 call); Frama_C_long_interval (0 call);
@@ -163,11 +163,11 @@
ungetc (0 call); unlink (0 call); usleep (0 call); utimes (0 call);
vfprintf (0 call); vfscanf (0 call); vprintf (0 call); vscanf (0 call);
vsnprintf (0 call); vsprintf (0 call); vsyslog (0 call); wait (0 call);
- waitpid (0 call); wcschr (0 call); wcscmp (0 call); wcscspn (0 call);
- wcslcat (0 call); wcslcpy (0 call); wcsncmp (0 call); wcspbrk (0 call);
- wcsrchr (0 call); wcsspn (0 call); wcsstr (0 call); wcstombs (0 call);
- wctomb (0 call); wmemchr (0 call); wmemcmp (0 call); wmemmove (0 call);
- write (0 call);
+ waitpid (0 call); wcscasecmp (0 call); wcschr (0 call); wcscmp (0 call);
+ wcscspn (0 call); wcslcat (0 call); wcslcpy (0 call); wcsncmp (0 call);
+ wcspbrk (0 call); wcsrchr (0 call); wcsspn (0 call); wcsstr (0 call);
+ wcstombs (0 call); wctomb (0 call); wmemchr (0 call); wmemcmp (0 call);
+ wmemmove (0 call); write (0 call);
Undefined and unspecified functions (1)
=======================================
@@ -195,7 +195,7 @@
Goto = 97
Assignment = 459
Exit point = 83
- Function = 497
+ Function = 498
Function call = 93
Pointer dereferencing = 159
Cyclomatic complexity = 296
diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle
index be0c42e7531..1115f88c003 100644
--- a/tests/libc/oracle/fc_libc.1.res.oracle
+++ b/tests/libc/oracle/fc_libc.1.res.oracle
@@ -6789,6 +6789,14 @@ extern wchar_t *fgetws(wchar_t * __restrict ws, int n,
}
*/
+/*@ requires valid_wstring_ws1: valid_read_wstring(ws1);
+ requires valid_wstring_ws2: valid_read_wstring(ws2);
+ assigns \result;
+ assigns \result
+ \from (indirect: *(ws1 + (0 ..))), (indirect: *(ws2 + (0 ..)));
+ */
+extern int wcscasecmp(wchar_t const *ws1, wchar_t const *ws2);
+
/*@ requires
valid_dest:
valid_or_empty((void *)dest, (unsigned int)(sizeof(wchar_t) * n));
diff --git a/tests/libc/oracle/wchar_h.res.oracle b/tests/libc/oracle/wchar_h.res.oracle
index bf863d20cc9..e224ff4e25b 100644
--- a/tests/libc/oracle/wchar_h.res.oracle
+++ b/tests/libc/oracle/wchar_h.res.oracle
@@ -185,6 +185,21 @@
[eva] tests/libc/wchar_h.c:66:
function wcsncat: no state left, precondition 'separation' got status valid.
[eva] Done for function wcsncat
+[eva] computing for function wcscasecmp <- main.
+ Called from tests/libc/wchar_h.c:70.
+[eva] using specification for function wcscasecmp
+[eva] tests/libc/wchar_h.c:70:
+ function wcscasecmp: precondition 'valid_wstring_ws1' got status valid.
+[eva] tests/libc/wchar_h.c:70:
+ function wcscasecmp: precondition 'valid_wstring_ws2' got status valid.
+[eva] Done for function wcscasecmp
+[eva] computing for function wcscasecmp <- main.
+ Called from tests/libc/wchar_h.c:71.
+[eva] tests/libc/wchar_h.c:71:
+ function wcscasecmp: precondition 'valid_wstring_ws1' got status valid.
+[eva] tests/libc/wchar_h.c:71:
+ function wcscasecmp: precondition 'valid_wstring_ws2' got status valid.
+[eva] Done for function wcscasecmp
[eva] Recording results for main
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
@@ -201,4 +216,5 @@
wdst2[0..9] ∈ {65}
[10] ∈ {0}
[11..19] ∈ [--..--]
+ ir ∈ [--..--]
__retres ∈ {0; 1}
diff --git a/tests/libc/wchar_h.c b/tests/libc/wchar_h.c
index e7cb493fa75..3bde71c8dc7 100644
--- a/tests/libc/wchar_h.c
+++ b/tests/libc/wchar_h.c
@@ -66,5 +66,8 @@ int main() {
wcsncat(wdst2+10, wdst2, 10); // error: no separation
//@ assert unreachable:\false;
}
+
+ int ir = wcscasecmp(L"\0", L"\0");
+ ir = wcscasecmp(wsrc, L"\0");
return 0;
}
--
GitLab