diff options
| author | Christophe Grenier <grenier@cgsecurity.org> | 2024-05-18 16:16:04 +0200 |
|---|---|---|
| committer | Christophe Grenier <grenier@cgsecurity.org> | 2024-05-18 16:16:04 +0200 |
| commit | 3df8ae06e9d6a21fd2f6ac55d93c8a1f178adfd8 (patch) | |
| tree | 22498060a4515b80af4b975e6c67c57a4281a59c /src | |
| parent | 0b989cc1ea3fbec6c5d324083c21788d0fe1471f (diff) | |
src/memmem.h: Add Frama-C annotations to td_memmem(), so Frama-C can
ssert the function terminates
Diffstat (limited to 'src')
| -rw-r--r-- | src/memmem.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/memmem.h b/src/memmem.h index d139d851..39b55dd2 100644 --- a/src/memmem.h +++ b/src/memmem.h @@ -52,6 +52,7 @@ static inline const void *td_memmem(const void *haystack, const unsigned int hay @ loop invariant \valid_read(begin); @ loop invariant \subset(begin, (char *)haystack+(0..haystack_len-needle_len+1)); @ loop assigns begin; + @ loop variant last_possible - begin; @*/ for (begin = (const char *) haystack; begin <= last_possible; ++begin) { |