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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
/*@-paramuse@*/
typedef struct
{
char *name;
char *id;
int year;
} record;
extern void allocYear (/*@special@*/ record *r)
/*@allocates r->year@*/ /* 1. Allocates clause includes *<parameter 1>.year of ... */
{
r->year = 23;
} /* 2. Unallocated storage r->year corresponds to storage listed ... */
extern void setName (/*@special@*/ record *r, /*@only@*/ char *name)
/*@defines r->name@*/
{
r->name = name;
}
extern void setName1 (/*@special@*/ record *r, /*@only@*/ char *name)
/*@defines r->name@*/
{
free (name);
} /* 3. Storage r->name listed in defines clause not defined at ... */
extern void setName2 (/*@special@*/ record *r, char *name)
/*@sets r->name@*/
{
strcpy (r->name, name);
}
extern void setName3 (/*@special@*/ record *r, char *name)
/*@sets r->name@*/
{
} /* 4. Storage *(r->name) listed in sets clause not defined at ... */
extern void setName4 (/*@special@*/ record *r, /*@only@*/ char *name)
/*@sets r->name@*/
{
r->name = name; /* 5. Implicitly only storage r->name not released before ... */
}
extern void allocName (/*@special@*/ record *r)
/*@allocates r->name@*/
{
r->name = (char *) malloc (sizeof (char) * 20);
}
extern void allocName2 (/*@special@*/ record *r)
/*@allocates r->name@*/
{
} /* 6. Storage r->name listed in allocates clauses is not ... */
extern void freeName (/*@special@*/ record r)
/*@releases r.name@*/
{
free (r.name);
}
extern void freeName2 (/*@special@*/ record r)
/*@releases r.name@*/
{
} /* 7. Storage r.name listed in releases clause not released */
extern void freeName3 (/*@special@*/ record *r)
/*@releases r->name@*/
{
free (r->name);
}
extern void freeName4 (/*@special@*/ record *r)
/*@releases r->name@*/
{
} /* 8. Storage r->name listed in releases clause not released ... */
|
