1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
|
/*
File: memmem.h
Copyright (C) 2005-2007 Christophe GRENIER <grenier@cgsecurity.org>
Copyright (C) 1991,92,93,94,96,97,98,2000,2004 Free Software Foundation, Inc.
The function has been copied from glibc 2.7
This software is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License along
with this program; if not, write the Free Software Foundation, Inc., 51
Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*/
#ifndef _MEMMEM_H
#define _MEMMEM_H
/*@
@ requires \valid_read((const char *)haystack+(0..haystack_len-1));
@ requires \valid_read((const char *)needle+(0..needle_len-1));
@ assigns \nothing;
@ ensures result_null_or_in_haystack:
@ \result == \null
@ || (\subset((char *)\result, (char *)haystack+(0..haystack_len-needle_len)) && \valid_read((char *)\result));
@*/
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;
const char *const last_possible = (const char *) haystack + haystack_len - needle_len;
if (needle_len == 0)
/* The first occurrence of the empty string is deemed to occur at
the beginning of the string. */
/*@ assert (\subset((char *)haystack, (char *)haystack+(0..haystack_len-needle_len)) && \valid_read((char *)haystack)); */
return (const void *) haystack;
/* Sanity check, otherwise the loop might search through the whole
memory. */
if (haystack_len < needle_len)
return NULL;
/*@
@ loop invariant \valid_read(begin);
@ loop invariant \subset(begin, (char *)haystack+(0..haystack_len-needle_len+1));
@ loop assigns begin;
@*/
for (begin = (const char *) haystack; begin <= last_possible; ++begin)
{
if (begin[0] == ((const char *) needle)[0] &&
!memcmp ((const void *) &begin[1],
(const void *) ((const char *) needle + 1),
needle_len - 1))
{
/*@ assert (\subset(begin, (char *)haystack+(0..haystack_len-needle_len)) && \valid_read(begin)); */
return (const void *) begin;
}
}
return NULL;
}
#endif
|
