test/constannot.c

   1 /*@constant int MaxLength=20@*/
   2 # define MaxLength 20
   3
   4 void foo (char *str) /*@requires maxSet(str) >= MaxLength@*/
   5 {
   6   str[20] = 'a';
   7 }
   8
   9 void foo2 (char *str) /*@requires maxSet(str) >= (MaxLength - 1)@*/
  10 {
  11   str[20] = 'a'; /* error */
  12 }
  13
  14 void foo3 ()
  15 {
  16   char buf[MaxLength];
  17
  18   buf[0] = '\0';
  19
  20   foo (buf); /* error: off by 1 */
  21   foo2 (buf); /* okay */
  22 }