diff options
| author | Christophe Grenier <[email protected]> | 2021-11-20 11:26:50 +0100 |
|---|---|---|
| committer | Christophe Grenier <[email protected]> | 2021-11-20 11:26:50 +0100 |
| commit | b2a0d41da609e62865beec1ed6faddd12bb5bdb8 (patch) | |
| tree | 2312b72445a9bce2e2c4790fb088d24bc030e90c /src/memmem.h | |
| parent | edcb650063911b563486bbbc54d62810145ca58b (diff) | |
Numerous frama-c annotations
Diffstat (limited to 'src/memmem.h')
| -rw-r--r-- | src/memmem.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/memmem.h b/src/memmem.h index 3ce9787d..d139d851 100644 --- a/src/memmem.h +++ b/src/memmem.h @@ -40,6 +40,7 @@ static inline const void *td_memmem(const void *haystack, const unsigned int hay 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 @@ -48,9 +49,12 @@ static inline const void *td_memmem(const void *haystack, const unsigned int hay 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), @@ -59,6 +63,7 @@ static inline const void *td_memmem(const void *haystack, const unsigned int hay /*@ assert (\subset(begin, (char *)haystack+(0..haystack_len-needle_len)) && \valid_read(begin)); */ return (const void *) begin; } + } return NULL; } #endif |