home *** CD-ROM | disk | FTP | other *** search
/ OS/2 Shareware BBS: 10 Tools / 10-Tools.zip / splint3s.zip / splint-3.0.1.6 / test / fields2.c < prev    next >
C/C++ Source or Header  |  2000-06-12  |  1KB  |  48 lines
  1. typedef struct 
  2. {
  3.   int *x;
  4.   int *y;
  5.   /*@dependent@*/ int *z;
  6. } *pair;
  7.  
  8. extern void pair_keep (/*@keep@*/ pair p);
  9.  
  10. extern /*@only@*/ /*@out@*/ void *smalloc (size_t);
  11. extern /*@partial@*/ pair pair_part (void);
  12.  
  13. /*@only@*/ pair pair_copy (pair p)
  14. {
  15.   pair ret = (pair) smalloc (sizeof (*ret));
  16.  
  17.   ret->x = p->x;
  18.   ret->y = p->y;
  19.   ret->z = p->z;
  20.  
  21.   return (ret); /* 1. Storage p->x reachable from parameter is kept (should be only) */
  22. }               /* 2. Storage p->y reachable from parameter is kept (should be only) */
  23.  
  24. /*@only@*/ pair pair_create (void)
  25. {
  26.   pair p = (pair) smalloc (sizeof (*p));
  27.  
  28.   p->x = smalloc (sizeof (int));
  29.   p->y = smalloc (sizeof (int));
  30.   p->z = p->y; /* 3. Only storage p->y assigned to dependent: p->z = p-y */
  31.  
  32.   *(p->x) = 3;
  33.   *(p->y) = 12;
  34.  
  35.   return p; /* 4. Storage p->y reachable from return value is unqualified */
  36. }
  37.  
  38. pair pair_swankle (/*@keep@*/ pair p)
  39. {
  40.   pair ret = pair_part ();
  41.  
  42.   ret->x = p->x;
  43.   pair_keep (p); /* 5. Storage p->x reachable from passed parameter is kept */ 
  44.   p->x = smalloc (sizeof (int));
  45.   *p->x = 3;
  46.   return ret;
  47. }
  48.