X-Git-Url: http://andersk.mit.edu/gitweb/splint.git/blobdiff_plain/413205495ba86eba68b461fce4eb1060273b53c3..d9a287624434f456bc3b1d8d8edf602ad5945cf9:/test/simplebufferConstraintTests/sizeof.c?ds=sidebyside

diff --git a/test/simplebufferConstraintTests/sizeof.c b/test/simplebufferConstraintTests/sizeof.c
index d95b92b..635601c 100644
--- a/test/simplebufferConstraintTests/sizeof.c
+++ b/test/simplebufferConstraintTests/sizeof.c
@@ -2,11 +2,11 @@
 extern void /*@alt char * @*/
   mystrncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2,
 size_t n) 
-  /*@modifies *s1@*/      /*@bufferConstraint MaxSet(s1) >= ( n - 1
-); MaxRead (s2) >= ( n - 1 ); @*/ /*@ensuresConstraint MaxRead (s1) ==
-MaxRead (s2); MaxRead (s1) <= n; @*/; 
+  /*@modifies *s1@*/      /*@requires MaxSet(s1) >= ( n - 1) /\ MaxRead (s2) >= ( n - 1 ); @*/ /*@ensures MaxRead (s1) ==
+MaxRead (s2) /\ MaxRead (s1) <= n; @*/; 
 
- void f(char *z) /*@bufferConstraint MaxRead(z) >= 2; @*/
+
+ void f(char *z) /*@requires MaxRead(z) >= 2; @*/
 {
 char x[3];
 char y[3];