]>
Commit | Line | Data |
---|---|---|
b9904f57 | 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 | } |