From 97cfc41e55639256f4b2ff089cf6d2f65bb23600 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 26 Sep 2024 14:24:25 +0200
Subject: [PATCH] [Libc] undefine 'index'/'rindex' if POSIX >= 200809
---
share/libc/strings.h | 4 ++
tests/builtins/oracle/memcpy.0.res.oracle | 8 ++--
...gs_h.res.oracle => strings_h.0.res.oracle} | 48 +++++++++----------
tests/libc/oracle/strings_h.1.res.oracle | 11 +++++
tests/libc/strings_h.c | 9 ++++
5 files changed, 52 insertions(+), 28 deletions(-)
rename tests/libc/oracle/{strings_h.res.oracle => strings_h.0.res.oracle} (83%)
create mode 100644 tests/libc/oracle/strings_h.1.res.oracle
diff --git a/share/libc/strings.h b/share/libc/strings.h
index ee25b389858..24ff2e7cfcd 100644
--- a/share/libc/strings.h
+++ b/share/libc/strings.h
@@ -52,6 +52,9 @@ extern void bzero(void *s, size_t n);
*/
extern int ffs(int i);
+#if _POSIX_C_SOURCE < 200809L
+// index and rindex were removed in POSIX-1.2008
+
/*@
assigns \result \from s, indirect:s[0 .. strlen(s)], indirect:c;
*/
@@ -61,6 +64,7 @@ extern char *index(const char *s, int c);
assigns \result \from s, indirect:s[0 .. strlen(s)], indirect:c;
*/
extern char *rindex(const char *s, int c);
+#endif
/*@
requires valid_string_s1: valid_read_string(s1);
diff --git a/tests/builtins/oracle/memcpy.0.res.oracle b/tests/builtins/oracle/memcpy.0.res.oracle
index 4f0cb38f1d5..3f3237a3c0e 100644
--- a/tests/builtins/oracle/memcpy.0.res.oracle
+++ b/tests/builtins/oracle/memcpy.0.res.oracle
@@ -1814,7 +1814,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 56)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 59)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1825,7 +1825,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 61)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 64)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1836,7 +1836,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 68)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 72)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
@@ -1847,7 +1847,7 @@
[ Extern ] Assigns nothing
Unverifiable but considered Valid.
-[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 75)
+[ Extern ] Froms (file FRAMAC_SHARE/libc/strings.h, line 79)
Unverifiable but considered Valid.
[ Valid ] Default behavior
by Frama-C kernel.
diff --git a/tests/libc/oracle/strings_h.res.oracle b/tests/libc/oracle/strings_h.0.res.oracle
similarity index 83%
rename from tests/libc/oracle/strings_h.res.oracle
rename to tests/libc/oracle/strings_h.0.res.oracle
index 291159bf7a4..4683c96f640 100644
--- a/tests/libc/oracle/strings_h.res.oracle
+++ b/tests/libc/oracle/strings_h.0.res.oracle
@@ -5,63 +5,63 @@
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
[eva] computing for function strcasecmp <- main.
- Called from strings_h.c:9.
+ Called from strings_h.c:15.
[eva] using specification for function strcasecmp
-[eva] strings_h.c:9:
+[eva] strings_h.c:15:
function strcasecmp: precondition 'valid_string_s1' got status valid.
-[eva] strings_h.c:9:
+[eva] strings_h.c:15:
function strcasecmp: precondition 'valid_string_s2' got status valid.
[eva] Done for function strcasecmp
[eva] computing for function strcasecmp <- main.
- Called from strings_h.c:10.
-[eva] strings_h.c:10:
+ Called from strings_h.c:16.
+[eva] strings_h.c:16:
function strcasecmp: precondition 'valid_string_s1' got status valid.
-[eva] strings_h.c:10:
+[eva] strings_h.c:16:
function strcasecmp: precondition 'valid_string_s2' got status valid.
[eva] Done for function strcasecmp
[eva] computing for function strcasecmp <- main.
- Called from strings_h.c:11.
-[eva] strings_h.c:11:
+ Called from strings_h.c:17.
+[eva] strings_h.c:17:
function strcasecmp: precondition 'valid_string_s1' got status valid.
-[eva] strings_h.c:11:
+[eva] strings_h.c:17:
function strcasecmp: precondition 'valid_string_s2' got status valid.
[eva] Done for function strcasecmp
[eva] computing for function strcasecmp <- main.
- Called from strings_h.c:12.
-[eva] strings_h.c:12:
+ Called from strings_h.c:18.
+[eva] strings_h.c:18:
function strcasecmp: precondition 'valid_string_s1' got status valid.
-[eva:alarm] strings_h.c:12: Warning:
+[eva:alarm] strings_h.c:18: Warning:
function strcasecmp: precondition 'valid_string_s2' got status invalid.
[eva] Done for function strcasecmp
[eva] computing for function strncasecmp <- main.
- Called from strings_h.c:13.
+ Called from strings_h.c:19.
[eva] using specification for function strncasecmp
-[eva] strings_h.c:13:
+[eva] strings_h.c:19:
function strncasecmp: precondition 'valid_string_s1' got status valid.
-[eva] strings_h.c:13:
+[eva] strings_h.c:19:
function strncasecmp: precondition 'valid_string_s2' got status valid.
[eva] Done for function strncasecmp
[eva] computing for function strncasecmp <- main.
- Called from strings_h.c:14.
-[eva] strings_h.c:14:
+ Called from strings_h.c:20.
+[eva] strings_h.c:20:
function strncasecmp: precondition 'valid_string_s1' got status valid.
-[eva:alarm] strings_h.c:14: Warning:
+[eva:alarm] strings_h.c:20: Warning:
function strncasecmp: precondition 'valid_string_s2' got status invalid.
[eva] Done for function strncasecmp
[eva] computing for function strncasecmp <- main.
- Called from strings_h.c:15.
-[eva] strings_h.c:15:
+ Called from strings_h.c:21.
+[eva] strings_h.c:21:
function strncasecmp: precondition 'valid_string_s1' got status valid.
-[eva] strings_h.c:15:
+[eva] strings_h.c:21:
function strncasecmp: precondition 'valid_string_s2' got status valid.
[eva] Done for function strncasecmp
[eva] computing for function bzero <- main.
- Called from strings_h.c:18.
+ Called from strings_h.c:24.
[eva] using specification for function bzero
-[eva] strings_h.c:18:
+[eva] strings_h.c:24:
function bzero: precondition 'valid_memory_area' got status valid.
[eva] Done for function bzero
-[eva] strings_h.c:19: assertion got status valid.
+[eva] strings_h.c:25: assertion got status valid.
[eva] Recording results for main
[eva] Done for function main
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/libc/oracle/strings_h.1.res.oracle b/tests/libc/oracle/strings_h.1.res.oracle
new file mode 100644
index 00000000000..714fee2dc3e
--- /dev/null
+++ b/tests/libc/oracle/strings_h.1.res.oracle
@@ -0,0 +1,11 @@
+[kernel] Parsing strings_h.c (with preprocessing)
+[kernel] strings_h.c:29: User Error:
+ Inconsistent storage specification for index. Previous declaration: FRAMAC_SHARE/libc/strings.h:61
+[kernel] strings_h.c:29: User Error:
+ Declaration of index does not match previous declaration from FRAMAC_SHARE/libc/strings.h:61 (different type constructors:
+ char *(char const *s, int c) and int).
+ 27
+ 28 // Check that 'index' is not defined when _POSIX_C_SOURCE >= 200809L
+ 29 static int index = 42;
+ ^^^^^
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/libc/strings_h.c b/tests/libc/strings_h.c
index 587b961e6ef..7b0d60d8542 100644
--- a/tests/libc/strings_h.c
+++ b/tests/libc/strings_h.c
@@ -1,3 +1,9 @@
+/* run.config
+ STDOPT: #"-cpp-extra-args=\"-D_POSIX_C_SOURCE=200809L\""
+ EXIT: 1
+ STDOPT:
+*/
+
#include <strings.h>
volatile int nondet;
@@ -18,3 +24,6 @@ void main() {
bzero(s4, 10);
//@ assert s4[9] == s4[8] == 0;
}
+
+// Check that 'index' is not defined when _POSIX_C_SOURCE >= 200809L
+static int index = 42;
--
GitLab