[Libc] undefine 'index'/'rindex' if POSIX >= 200809

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);

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.

tests/libc/oracle/strings_h.res.oracle → 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 ======

tests/libc/oracle/strings_h.1.res.oracle

+[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.

tests/libc/strings_h.c

+/* 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;