Changed to used /\ and requires instead of bufferConstraint

[splint.git] / test / simplebufferConstraintTests / m.c

diff --git a/test/simplebufferConstraintTests/m.c b/test/simplebufferConstraintTests/m.c
index 129144dfdbb9bf57db61956dc3eb81cb65fa7ca5..9c0636f3728ec0351c1f1c0d36471339426cc424 100644 (file)
--- a/test/simplebufferConstraintTests/m.c
+++ b/test/simplebufferConstraintTests/m.c
@@ -1,5 +1,5 @@
 extern /*@null@*/ /*@out@*/ /*@only@*/ void *mymalloc (size_t size) /*@*/
-     /*@ensuresConstraint MaxSet(result) == (size - 1); @*/ ;
+     /*@ensures MaxSet(result) == (size - 1) @*/ ;
   
 void t()
 {