*** empty log message ***

[splint.git] / test / maxset / maxsetannotations.c

diff --git a/test/maxset/maxsetannotations.c b/test/maxset/maxsetannotations.c
index fdf928835e01e27457c73e55dec05dfb4e9a73a3..503ffdda6b5c76b0dd6f0ab33e134289c3fec572 100644 (file)
--- a/test/maxset/maxsetannotations.c
+++ b/test/maxset/maxsetannotations.c
@@ -1,6 +1,6 @@
 #include "../../lib/ansi.h"
 
-void anstrcpy( /*@unique@*/ char * a, char *b) /*@LRequires MaxSet(a) >= MaxRead (b); @*/ {
+void anstrcpy( /*@unique@*/ char * a, char *b) /*@requires MaxSet(a) >= MaxRead (b); @*/ {
 strcpy (a,b);
 }