From 1c18777bf038a71ff0184c2dba3c675f0841c8a6 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Tue, 23 Jul 2019 09:04:26 +0200
Subject: [PATCH] [Libc] fix typo in ACSL specification
---
share/libc/string.h | 2 +-
tests/libc/oracle/fc_libc.1.res.oracle | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/share/libc/string.h b/share/libc/string.h
index c8f5b3d8ec3..566b296162c 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 46a7daf3a80..8d9222bf040 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)) ∨
--
GitLab