diff --git a/share/libc/string.h b/share/libc/string.h index c8f5b3d8ec308565caed422e7debcb744c61c755..566b296162caca8aebbd4466043550e300659bab 100644 --- a/share/libc/string.h +++ b/share/libc/string.h @@ -66,7 +66,7 @@ extern int memcmp (const void *s1, const void *s2, size_t n); /*@ requires valid: valid_read_or_empty(s, n) - || \valid_read(((unsigned char*)s)+(..memchr_off((char*)s,c,n))); + || \valid_read(((unsigned char*)s)+(0..memchr_off((char*)s,c,n))); @ requires initialization: \initialized(((unsigned char*)s)+(0..n - 1)) || \initialized(((unsigned char*)s)+(0..memchr_off((char*)s,c,n))); diff --git a/tests/libc/oracle/fc_libc.1.res.oracle b/tests/libc/oracle/fc_libc.1.res.oracle index 46a7daf3a80476931d58f62f30b136b84c6c7463..8d9222bf04041f16622c88a3d7fe6bbfba9f21c7 100644 --- a/tests/libc/oracle/fc_libc.1.res.oracle +++ b/tests/libc/oracle/fc_libc.1.res.oracle @@ -5431,7 +5431,7 @@ char *strrchr(char const *s, int c) /*@ requires valid: valid_read_or_empty(s, n) ∨ - \valid_read((unsigned char *)s + (.. memchr_off((char *)s, c, n))); + \valid_read((unsigned char *)s + (0 .. memchr_off((char *)s, c, n))); requires initialization: \initialized((unsigned char *)s + (0 .. n - 1)) ∨