[Libc] add prototype and spec for non-POSIX function memmem

share/libc/string.h

@@ -499,6 +499,21 @@ extern size_t strlcat(char *restrict dest, const char *restrict src, size_t n);
 extern size_t strxfrm (char *restrict dest,
 		       const char *restrict src, size_t n);
 
+// Non-POSIX; GNU extension
+/*@
+  requires valid_haystack: \valid_read((char*)haystack + (0 .. haystacklen-1));
+  requires valid_needle: \valid_read((char*)needle + (0 .. needlelen-1));
+  assigns \result \from haystack,
+                        indirect:((char*)haystack)[0 .. haystacklen-1],
+                        indirect:((char*)needle)[0 .. needlelen-1];
+  ensures result_null_or_valid:
+    \result == \null || \valid_read((char*)\result);
+  ensures result_null_or_same_base:
+    \result == \null || \base_addr(\result) == \base_addr(haystack);
+*/
+extern void *memmem(const void *haystack, size_t haystacklen,
+             const void *needle, size_t needlelen);
+
 // Allocate strings
 
 /*@ requires valid_string_s: valid_read_string(s);

tests/libc/string_h.c

@@ -174,5 +174,15 @@ int main(int argc, char **argv)
   rchr = memrchr(c, 'n', strlen(c));
   //@ check imprecise: rchr == \null;
 
+  char mm_haystack[] = { 'I', 'h', 'a', 'v', 'e', '\0', 'z', 'e', 'r', 'o' };
+  char mm_needle[] = { 'z', 'e', 'r', 'o' };
+  char *memm =
+    memmem(mm_haystack, sizeof(mm_haystack), mm_needle, sizeof(mm_needle));
+  //@ check imprecise: memm == mm_haystack + 6;
+  char mm_needle2[] = { '0' };
+  memm =
+    memmem(mm_haystack, sizeof(mm_haystack), mm_needle2, sizeof(mm_needle2));
+  //@ check imprecise: memm == \null;
+
   return 0;
 }