*** empty log message ***

[splint.git] / lib / ansi.h

diff --git a/lib/ansi.h b/lib/ansi.h
index 5a80fd29c8519a84022a1f0735645b82ac792b4a..51925b15c46eaff18722590911d27e09cad60d07 100644 (file)
--- a/lib/ansi.h
+++ b/lib/ansi.h
@@ -847,13 +847,13 @@ extern size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n)
 extern void /*@alt void * @*/
   memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n) 
   /*@modifies *s1@*/
-     /*@requires MaxRead(s2) >= n /\ MaxSet(s1) >= n; @*/
+     /*@requires MaxRead(s2) >= (n - 1) /\ MaxSet(s1) >= (n - 1); @*/
      ;
 
 extern void /*@alt void * @*/
   memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n)
   /*@modifies *s1@*/
-  /*@requires MaxRead(s2) >= n /\ MaxSet(s1) >= n; @*/
+  /*@requires MaxRead(s2) >= (n - 1) /\ MaxSet(s1) >= (n - 1); @*/
    ;