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