From a22838dd83079efd1852b1a82ee16b25233c5fc5 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 18 Mar 2024 16:39:58 +0100
Subject: [PATCH] [Libc] add prototype and spec for non-POSIX function memmem
---
share/libc/string.h | 15 +++++++++++++++
tests/libc/string_h.c | 10 ++++++++++
2 files changed, 25 insertions(+)
diff --git a/share/libc/string.h b/share/libc/string.h
index d021f5a873f..0d6379e24f0 100644
--- a/share/libc/string.h
+++ b/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);
diff --git a/tests/libc/string_h.c b/tests/libc/string_h.c
index d51e38c9c28..090b9f60561 100644
--- a/tests/libc/string_h.c
+++ b/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;
}
--
GitLab