X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/2ab9c885b11ea2ed5e45af61e728e20d6979f745..dcaf75eaed37623f27c23241c146ad25910208f3:/test/globalbufferannotation/globalvariable.c

diff --git a/test/globalbufferannotation/globalvariable.c b/test/globalbufferannotation/globalvariable.c
index 817dcd2..75efab9 100644
--- a/test/globalbufferannotation/globalvariable.c
+++ b/test/globalbufferannotation/globalvariable.c
@@ -3,10 +3,10 @@
 static char f [12];
 extern void /*@alt char * @*/
   mstrcpy (/*@unique@*/ /*@out@*/ /*returned*/ char *s1, char *s2) 
-     /*@modifies *s1@*/ /*@bufferConstraint MaxSet(s1) >= MaxRead(s2); @*/;
+     /*@modifies *s1@*/ /*@requires MaxSet(s1) >= MaxRead(s2); @*/;
 
 
-void copyf (char * c) /*@bufferConstraint MaxSet(c) >= MaxRead(f); @*/
+void copyf (char * c) /*@requires MaxSet(c) >= MaxRead(f); @*/
 {
   mstrcpy (c, f);
 }