]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | # include "modifies.h" |
2 | ||
3 | static int mstat; | |
4 | static /*@unused@*/ int internalState; | |
5 | ||
6 | int f3 (int p[]) | |
928377c6 | 7 | /*@modifies |
8 | internalState, fileSystem;@*/ ; /* 1. Modifies list uses ... */ | |
885824d3 | 9 | |
10 | int f4 (int p[]) | |
11 | /*@modifies p[3];@*/; | |
12 | ||
13 | int f5 (int fileSystem) | |
14 | /*@modifies fileSystem;@*/ ; /* 2. Modifies list uses fileSystem ... */ | |
15 | ||
16 | int f6 (void); | |
17 | ||
18 | int f6 (void) /*@modifies mstat;@*/ /* 3. Implementation modifies list for ... */ | |
19 | { | |
20 | return (mstat++); | |
21 | } | |
22 | ||
23 | int f1 (/*@unused@*/ int p[]) | |
24 | { | |
25 | mstat++; /* 4. Suspect modification of mstat: mstat++ */ | |
26 | return mstat; | |
27 | } | |
28 | ||
29 | int f2 (/*@unused@*/ int p[]) /*@modifies mstat;@*/ | |
30 | { | |
31 | mstat++; | |
32 | return 3; | |
33 | } | |
34 | ||
35 | int g2 (/*@unused@*/ int p[]) | |
36 | { | |
37 | return 3; | |
38 | } /* 5. Function g2 specified to modify internal state but no internal */ |