]>
Commit | Line | Data |
---|---|---|
80ee600a | 1 | extern int glob; |
2 | ||
3 | /*@function int fg(void) globals glob;@*/ | |
4 | # define fg() (glob + 1) | |
5 | ||
6 | /*@function int fm(void) globals glob; modifies glob;@*/ | |
7 | # define fm() (glob++) | |
8 | ||
9 | int f (void) /*@globals undef glob@*/ ; | |
10 | ||
11 | int f (void) /*@globals undef glob@*/ | |
12 | { | |
13 | return glob; | |
14 | } | |
15 | # if 0 | |
16 | int f2 (void) /*@globals int glob;@*/ | |
17 | { | |
18 | return glob; | |
19 | } | |
20 | # endif |