assign7.c

/* run.config
   OPT: -rte -warn-signed-overflow -print -journal-disable
*/

//@ assigns *p \from \union(*(char*)p,*q);
extern void f(int* p, int* q);

//@ assigns *p \from \union(*p, \union(*r,*q));
extern void ff(int* p, int* q, int* r);

//@ assigns *p \from \inter(*(char*)p,*q);
extern void h(int* p, int* q);

//@ assigns \union(*p,*q);
extern void g(int* p, int* q);

/*@ assigns \at(*p,Post), \at(*p,Pre), *p ;
 */
extern void gg(int* p);

int X, Y ;
//@ assigns \union(X, Y) ;
void hh(void);

int main() {
  int x,y,z;
  f(&x,&y);
  ff(&x,&y,&z);
  g(&x,&y);
  h(&x,&y);
  gg(&x);
  hh();
}