home
***
CD-ROM
|
disk
|
FTP
|
other
***
search
/
OS/2 Shareware BBS: 10 Tools
/
10-Tools.zip
/
lclint.zip
/
lclint-2_3h-os2-bin.zip
/
test
/
specclauses5.c
< prev
next >
Wrap
C/C++ Source or Header
|
1997-09-03
|
937b
|
53 lines
/*@-paramuse@*/
typedef struct
{
int id;
char *name;
} *record;
/*@special@*/ record newrecord (void)
/*@defines result@*/
/*@post:isnull result->name@*/
{
record r = (record) malloc (sizeof (*r));
assert (r != NULL);
r->id = 3;
r->name = NULL;
return r;
}
record createrecord (/*@only@*/ char *name)
{
record r = newrecord ();
r->name = name;
return r;
}
record createrecord2 (void)
{
record r = newrecord ();
return r; /* 1. Null storage r->name derivable from return value: r */
}
/*@special@*/ record newrecord2 (void)
/*@defines *result@*/
/*@post:observer result->name@*/
{
record r = (record) malloc (sizeof (*r));
assert (r != NULL);
r->id = 3;
r->name = NULL;
return r; /* 2. Non-observer storage r->name corresponds to storage ... */
}
record createrecordx (void)
{
record r = newrecord2 ();
return r; /* 3. Observer storage r->name reachable from observer return */
}