home *** CD-ROM | disk | FTP | other *** search
/ OS/2 Shareware BBS: 10 Tools / 10-Tools.zip / splint3s.zip / splint-3.0.1.6 / test / constannot.c < prev    next >
Text File  |  2001-07-24  |  361b  |  23 lines
  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. }
  23.