1 /*@constant int MaxLength=20@*/
4 void foo (char *str) /*@requires maxSet(str) >= MaxLength@*/
9 void foo2 (char *str) /*@requires maxSet(str) >= (MaxLength - 1)@*/
11 str[20] = 'a'; /* error */
20 foo (buf); /* error: off by 1 */
21 foo2 (buf); /* okay */