summaryrefslogtreecommitdiffstats
path: root/src/memmem.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/memmem.h')
-rw-r--r--src/memmem.h8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/memmem.h b/src/memmem.h
index d738dba..caa6873 100644
--- a/src/memmem.h
+++ b/src/memmem.h
@@ -22,6 +22,11 @@
*/
+/*@
+ @ requires \valid_read((const char *)haystack+(0..haystack_len-1));
+ @ requires \valid_read((const char *)needle+(0..needle_len-1));
+ @ assigns \nothing;
+ @*/
static inline const void *td_memmem(const void *haystack, const unsigned int haystack_len, const void *needle, const unsigned int needle_len)
{
const char *begin;
@@ -37,6 +42,9 @@ static inline const void *td_memmem(const void *haystack, const unsigned int hay
if (haystack_len < needle_len)
return NULL;
+ /*@
+ @ loop assigns begin;
+ @*/
for (begin = (const char *) haystack; begin <= last_possible; ++begin)
if (begin[0] == ((const char *) needle)[0] &&
!memcmp ((const void *) &begin[1],